2013 | OriginalPaper | Buchkapitel
A Data Driven Approach for Algebraic Loop Invariants
verfasst von : Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, Aditya V. Nori
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We describe a
Guess-and-Check
algorithm for computing algebraic equation invariants of the form ∧
i
f
i
(
x
1
,…,
x
n
) = 0, where each
f
i
is a polynomial over the variables
x
1
,…,
x
n
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 efficiently compute algebraic invariants in all cases, with only a few tests.