Using dynamic analysis to generate disjunctive invariants

Thanh Vu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest

Research output: Contribution to journalConference article

16 Citations (Scopus)

Abstract

Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ''max-plus'' and ''min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.

Original languageEnglish (US)
Pages (from-to)608-619
Number of pages12
JournalProceedings - International Conference on Software Engineering
Issue number1
DOIs
StatePublished - May 31 2014
Externally publishedYes
Event36th International Conference on Software Engineering, ICSE 2014 - Hyderabad, India
Duration: May 31 2014Jun 7 2014

Fingerprint

Dynamic analysis
Theorem proving
Surface mount technology
Algebra
Repair
Semantics
Costs
Defect detection

Keywords

  • disjunctive invariants
  • invariant generation
  • Program analysis
  • static and dynamic analyses
  • theorem proving

ASJC Scopus subject areas

  • Software

Cite this

Using dynamic analysis to generate disjunctive invariants. / Nguyen, Thanh Vu; Kapur, Deepak; Weimer, Westley; Forrest, Stephanie.

In: Proceedings - International Conference on Software Engineering, No. 1, 31.05.2014, p. 608-619.

Research output: Contribution to journalConference article

@article{9e8d9caab03047b29296d537cf9e5d16,
title = "Using dynamic analysis to generate disjunctive invariants",
abstract = "Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ''max-plus'' and ''min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.",
keywords = "disjunctive invariants, invariant generation, Program analysis, static and dynamic analyses, theorem proving",
author = "Nguyen, {Thanh Vu} and Deepak Kapur and Westley Weimer and Stephanie Forrest",
year = "2014",
month = "5",
day = "31",
doi = "10.1145/2568225.2568275",
language = "English (US)",
pages = "608--619",
journal = "Proceedings - International Conference on Software Engineering",
issn = "0270-5257",
publisher = "IEEE Computer Society",
number = "1",

}

TY - JOUR

T1 - Using dynamic analysis to generate disjunctive invariants

AU - Nguyen, Thanh Vu

AU - Kapur, Deepak

AU - Weimer, Westley

AU - Forrest, Stephanie

PY - 2014/5/31

Y1 - 2014/5/31

N2 - Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ''max-plus'' and ''min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.

AB - Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ''max-plus'' and ''min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.

KW - disjunctive invariants

KW - invariant generation

KW - Program analysis

KW - static and dynamic analyses

KW - theorem proving

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

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

U2 - 10.1145/2568225.2568275

DO - 10.1145/2568225.2568275

M3 - Conference article

AN - SCOPUS:84994176576

SP - 608

EP - 619

JO - Proceedings - International Conference on Software Engineering

JF - Proceedings - International Conference on Software Engineering

SN - 0270-5257

IS - 1

ER -