A Data Driven Approach for Algebraic Loop Invariants

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.