Verifying Programs via Iterated Specialization

We present a method for verifying properties of imperative pro-grams by using techniques based on the specialization of constraintlogic programs (CLP). We consider a class of C programs withinteger variables and we focus our attention on safety properties,stating that no error configuration can be reached from the initialconfigurations. We encode the interpreter of the language as a CLPprogramI, and we also encode the safety property to be verified asthe negation of a predicateunsafedefined inI. Then, we specializethe CLP programIwith respect to the given C program and thegiven initial and error configurations, with the objective of derivinga new CLP programIspwhich either contains the factunsafe(andin this case the C program is proved unsafe) or contains no clauseswith headunsafe(and in this case the C program is proved safe).IfIspdoes not enjoy this property we iterate the specialization pro-cess with the objective of deriving a CLP program where we canprove unsafety or safety. During the various specializations we mayapply different strategies for propagating information (either prop-agating forward from an initial configuration, or propagating back-ward from an error configuration) and different operators (such aswidening and convex hull operators) for generalizing predicate def-initions. Due to the undecidability of program safety, the iteratedspecialization process may not terminate. By an experimental eval-uation carried out on a set of examples taken from the literature, weshow that our method is competitive with respect to state-of-the-artsoftware model checkers.