TY - GEN
T1 - Using dynamic analysis to discover polynomial and array invariants
AU - Nguyen, Thanh Vu
AU - Kapur, Deepak
AU - Weimer, Westley
AU - Forrest, Stephanie
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
KW - array invariants
KW - dynamic analysis
KW - invariant generation
KW - nonlinear invariants
KW - program analysis
UR - http://www.scopus.com/inward/record.url?scp=84864217843&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84864217843&partnerID=8YFLogxK
U2 - 10.1109/ICSE.2012.6227149
DO - 10.1109/ICSE.2012.6227149
M3 - Conference contribution
AN - SCOPUS:84864217843
SN - 9781467310673
T3 - Proceedings - International Conference on Software Engineering
SP - 683
EP - 693
BT - Proceedings - 34th International Conference on Software Engineering, ICSE 2012
T2 - 34th International Conference on Software Engineering, ICSE 2012
Y2 - 2 June 2012 through 9 June 2012
ER -