Verification of Programs by Combining Iterated Specialization with Interpolation

We present a verification technique for program safety that combinesIterated SpecializationandInterpolating Horn Clause Solving. Our new method composes together these two techniques ina modular way by exploiting the common Horn Clause representation of the verification problem.The Iterated Specialization verifier transforms an initialset of verification conditions by using un-fold/fold equivalence preserving transformation rules. During transformation, program invariants arediscovered by applying widening operators. Then the outputset of specialized verification conditionsis analyzed by an Interpolating Horn Clause solver, hence adding the effect of interpolation to theeffect of widening. The specialization and interpolation phases can be iterated, and also combinedwith other transformations that change the direction of propagation of the constraints (forward fromthe program preconditions or backward from the error conditions). We have implemented our ver-ification technique by integrating the VeriMAP verifier withthe FTCLP Horn Clause solver, basedon Iterated Specialization and Interpolation, respectively. Our experimental results show that theintegrated verifier improves the precision of each of the individual components run separately.