Finding Loop Invariants Using a Theorem Prover

This talk presents how quantified loop invariants of programs over arrays can be automatically inferred using a first order theorem prover, reducing the burden of annotating loops with complete invariants.

Our approach allows one to generate first-order invariants containing alternations of quantifiers.
For doing so, we deploy symbolic computation methods to generate numeric invariants of the scalar loop variables, based on the software package Aligator, and then use update predicates of the loop. 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. The first-order information extracted from the loop description can use auxiliary symbols, such as symbols denoting update predicates or loop counters. After having collected the first-order information, we run the saturation theorem prover Vampire to eliminate the auxiliary symbols and obtain loop invariants expressed as first-order formulas. When the invariants obtained in this way contain skolem functions, we de-skolemise them into formulas with quantifier alternations.

Our method does not require the user to give a post-condition, a predefined collection of predicates or any other form of human guidance and avoids inductive reasoning.

This is a joint work with
Andrei Voronkov (University of Manchester, UK).

Speaker Details

Laura Kovács is a postdoctoral researcher in the Programming Methodology research group of Prof. Peter Mueller at ETH Zuerich, Switzerland. Her research deals with the design and development of new theories, technologies, and tools for program verification, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She holds an MSc from the Western University of Timisoara, Romania, and a PhD degree from the Research Institute for Symbolic Computation of the Johannes Kepler University, Linz, Austria. Before joining ETH Zurich, she was a postdoctoral researcher at EPFL, Switzerland, in the Models and Theory of Computation research group of Prof. Thomas A. Henzinger.url: http://mtc.epfl.ch/~likovacs/

Date:
Speakers:
Laura Kovacs
Affiliation:
ETH Zuerich, Switzerland