Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

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.

Published in:
Fundamental Approaches To Software Engineering, Proceedings, 5503, 470-485
Presented at:
12th International Conference on Fundamental Applroaches to Software Engineering held in Conjuction with European Conference on Theroy and Practice of Software, York, ENGLAND, Mar 22-29, 2009
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa

 Record created 2010-11-30, last modified 2018-03-17

Rate this document:

Rate this document:
(Not yet reviewed)