Finding Loop Invariants Using a Theorem Prover

Опубликовано 7 сентября 2016, 17:29

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