Details

Autor(en) / Beteiligte

• Kovács, Laura
• Voronkov, Andrei

Titel

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Ist Teil von

• Fundamental Approaches to Software Engineering, p.470-485

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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.