Sciweavers

Share
FASE
2009
Springer

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

12 years 11 days ago
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover
Abstract. We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on the automatic analysis of the so-called update predicates of loops. An update predicate for an array A expresses updates made to A. We observe that many properties of update predicates can be extracted automatically from the loop description and loop properties obtained by other methods such as a simple analysis of counters occurring in the loop, recurrence solving and quantifier elimination over loop variables. We run the theorem prover Vampire on some examples and show that non-trivial loop invariants can be generated.
Laura Kovács, Andrei Voronkov
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where FASE
Authors Laura Kovács, Andrei Voronkov
Comments (0)
books