Program Verification via Iterated Specialization

We present a method for verifying properties of imperative programs by using techniques basedon the specialization of constraint logic programs (CLP). We consider a class of imperativeprograms with integer variables and we focus our attention on safety properties, stating that noerror configuration can be reached from any initial configuration. We introduce a CLP programIthat encodes the interpreter of the language, and also defines a predicateunsafeequivalent tothe negation of the safety property to be verified. Then, we specialize the CLP programIwithrespect to the given imperative program and the given initial and error configurations, with theobjective of deriving a new CLP programIspthat either contains the factunsafe(and in thiscase the imperative program is proved unsafe) or contains noclauses with headunsafe(and inthis case the imperative program is proved safe). IfIspdoes not enjoy this property we iterate thespecialization process with the objective of deriving a CLPprogram where we can prove unsafetyor safety. During the various specializations we may apply different strategies for propagatinginformation (either propagating forward from an initial configuration to an error configuration,or propagating backward from an error configuration to an initial configuration) and differentoperators (such as the widening and convex hull operators) for generalizing predicate definitions.Each specialization step is guaranteed to terminate, but due to the undecidability of programsafety, the iterated specialization process may not terminate. By an experimental evaluationcarried out on a significant set of examples taken from the literature, we show that our methodimproves the precision of verification with respect to state-of-the-art software model checkers.