In this talk we describe how symbol elimination
in first-order theorem proving can be used as an alternative to interpolation and invariant generation for software verification.
For doing so, the talk will be divided in two parts.
In the first part of the talk we present a new technique for quantified invariant generation using a first-order theorem prover.
Our approach allows one to generate first-order invariants containing alternations of quantifiers.
To this end, we first deploy symbolic computation methods to generate numeric invariants of the scalar loop variables, based on the software package Aligator, and then use so-called update predicates over unbounded data structures, such as arrays.
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.
Symbol elimination is thus the main ingredient in generating quantified loop invariants by a first-order theorem prover.
In the second part of the talk, we present how interpolants can be automatically constructed from symbol-eliminating proofs.
The interpolants generated by our method are boolean combinations of conclusions of symbol eliminating inferences of a first-order resolution proof produced by Vampire.
This is a joint work with Krystof Hoder and Andrei Voronkov
(The University of Manchester).