@inproceedings{andgupta2013a,
author = { and Gupta, Saurabh and Hariharan, Bharath and Aiken, Alex and Liang, Percy and Nori, Aditya},
title = {A Data Driven Approach for Algebraic Loop Invariants},
booktitle = {European Symposium on Programming (ESOP)},
year = {2013},
month = {March},
abstract = {We describe a Guess-and-Check algorithm for computing algebraic equation invariants of the form wedge i fi(x1, ... , xn) = 0, where each fi is a polynomial over the variables x1, ... , xn of the program. The Guess phase is data driven and derives a candidate invariant from data generated from concrete executions of the program. This candidate invariant is subsequently validated in a Check phase by an off-the-shelf SMT solver. Iterating between the two phases leads to a sound algorithm. Moreover, we are able to prove a bound on the number of decision procedure queries which Guess-and-Check requires to obtain a sound invariant. We show how Guess-and-Check can be extended to generate arbitrary boolean combinations of linear equalities as invariants, which enables us to generate expressive invariants to be consumed by tools that cannot handle non-linear arithmetic. We have evaluated our technique on a number of benchmark programs from recent papers on invariant generation. Our results are encouraging – we are able to effifficiently compute algebraic invariants in all cases, with only a few tests.},
publisher = {Lecture Notes in Computer Science},
url = {http://approjects.co.za/?big=en-us/research/publication/a-data-driven-approach-for-algebraic-loop-invariants-2/},
edition = {European Symposium on Programming (ESOP)},
}