Verification of Programs by Combining Iterated Specialization with Interpolation

TL;DR

This paper introduces a modular verification technique that combines Iterated Specialization and Interpolating Horn Clause Solving to improve program safety verification accuracy.

Contribution

It presents a novel combined approach integrating specialization and interpolation for program verification, enhancing precision over individual methods.

Findings

Improved verification precision with combined approach

Effective discovery of program invariants

Enhanced analysis through iterative specialization and interpolation

Abstract

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.