Verification of Programs by Combining Iterated Specialization with Interpolation

Emanuele De Angelis
Fabio Fioravanti
Jorge A. Navas
Maurizio Proietti

We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause representation of the verification problem. The Iterated Specialization verifier transforms an initial set of verification conditions by using unfold/fold equivalence preserving transformation rules. During transformation, program invariants are discovered by applying widening operators. Then the output set of specialized verification conditions is analyzed by an Interpolating Horn Clause solver, hence adding the effect of interpolation to the effect of widening. The specialization and interpolation phases can be iterated, and also combined with other transformations that change the direction of propagation of the constraints (forward from the program preconditions or backward from the error conditions). We have implemented our verification technique by integrating the VeriMAP verifier with the FTCLP Horn Clause solver, based on Iterated Specialization and Interpolation, respectively. Our experimental results show that the integrated verifier improves the precision of each of the individual components run separately.

In Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko and Valerio Senni: Proceedings First Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014), Vienna, Austria, 17 July 2014, Electronic Proceedings in Theoretical Computer Science 169, pp. 3–18.
Published: 2nd December 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: