PRECIS

Inferring invariants using program path guided clustering

Parth Sagdeo, Viraj Athavale, Sumant Kowshik, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.

Original languageEnglish (US)
Title of host publication2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings
Pages532-535
Number of pages4
DOIs
StatePublished - Dec 1 2011
Event2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011 - Lawrence, KS, United States
Duration: Nov 6 2011Nov 10 2011

Publication series

Name2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

Other

Other2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011
CountryUnited States
CityLawrence, KS
Period11/6/1111/10/11

Fingerprint

Linear regression

ASJC Scopus subject areas

  • Software

Cite this

Sagdeo, P., Athavale, V., Kowshik, S., & Vasudevan, S. (2011). PRECIS: Inferring invariants using program path guided clustering. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings (pp. 532-535). [6100117] (2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings). https://doi.org/10.1109/ASE.2011.6100117

PRECIS : Inferring invariants using program path guided clustering. / Sagdeo, Parth; Athavale, Viraj; Kowshik, Sumant; Vasudevan, Shobha.

2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. p. 532-535 6100117 (2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Sagdeo, P, Athavale, V, Kowshik, S & Vasudevan, S 2011, PRECIS: Inferring invariants using program path guided clustering. in 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings., 6100117, 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings, pp. 532-535, 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Lawrence, KS, United States, 11/6/11. https://doi.org/10.1109/ASE.2011.6100117
Sagdeo P, Athavale V, Kowshik S, Vasudevan S. PRECIS: Inferring invariants using program path guided clustering. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. p. 532-535. 6100117. (2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings). https://doi.org/10.1109/ASE.2011.6100117
Sagdeo, Parth ; Athavale, Viraj ; Kowshik, Sumant ; Vasudevan, Shobha. / PRECIS : Inferring invariants using program path guided clustering. 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings. 2011. pp. 532-535 (2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings).
@inproceedings{959f39a6fd09404d87ff84e5785836fa,
title = "PRECIS: Inferring invariants using program path guided clustering",
abstract = "We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.",
author = "Parth Sagdeo and Viraj Athavale and Sumant Kowshik and Shobha Vasudevan",
year = "2011",
month = "12",
day = "1",
doi = "10.1109/ASE.2011.6100117",
language = "English (US)",
isbn = "9781457716393",
series = "2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings",
pages = "532--535",
booktitle = "2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings",

}

TY - GEN

T1 - PRECIS

T2 - Inferring invariants using program path guided clustering

AU - Sagdeo, Parth

AU - Athavale, Viraj

AU - Kowshik, Sumant

AU - Vasudevan, Shobha

PY - 2011/12/1

Y1 - 2011/12/1

N2 - We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.

AB - We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.

UR - http://www.scopus.com/inward/record.url?scp=84855431956&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84855431956&partnerID=8YFLogxK

U2 - 10.1109/ASE.2011.6100117

DO - 10.1109/ASE.2011.6100117

M3 - Conference contribution

SN - 9781457716393

T3 - 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

SP - 532

EP - 535

BT - 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

ER -