Using dynamic analysis to discover polynomial and array invariants

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

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

53 Scopus citations

Abstract

Dynamic invariant analysis identifies likely properties over variables from observed program traces. These properties can aid programmers in refactoring, documenting, and debugging tasks by making dynamic patterns visible statically. Two useful forms of invariants involve relations among polynomials over program variables and relations among array variables. Current dynamic analysis methods support such invariants in only very limited forms. We combine mathematical techniques that have not previously been applied to this problem, namely equation solving, polyhedra construction, and SMT solving, to bring new capabilities to dynamic invariant detection. Using these methods, we show how to find equalities and inequalities among nonlinear polynomials over program variables, and linear relations among array variables of multiple dimensions. Preliminary experiments on 24 mathematical algorithms and an implementation of AES encryption provide evidence that the approach is effective at finding these invariants.

Original languageEnglish (US)
Title of host publicationProceedings - 34th International Conference on Software Engineering, ICSE 2012
Pages683-693
Number of pages11
DOIs
StatePublished - Jul 30 2012
Externally publishedYes
Event34th International Conference on Software Engineering, ICSE 2012 - Zurich, Switzerland
Duration: Jun 2 2012Jun 9 2012

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Other

Other34th International Conference on Software Engineering, ICSE 2012
Country/TerritorySwitzerland
CityZurich
Period6/2/126/9/12

Keywords

  • array invariants
  • dynamic analysis
  • invariant generation
  • nonlinear invariants
  • program analysis

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Using dynamic analysis to discover polynomial and array invariants'. Together they form a unique fingerprint.

Cite this