Verifying Programs 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 C programswith integer variables and we focus our attention on safety properties, stating that no errorconfiguration can be reached from the initial configurations. We encode the interpreter of thelanguage as a CLP programI, and we also encode the safety property to be verified as thenegation of a predicateunsafedefined inI. Then, we specialize the CLP programIwithrespect to the given C program and the given initial and errorconfigurations, with the objectiveof deriving a new CLP programIspwhich either contains the factunsafe(and in this casethe C program is proved unsafe) or contains no clauses with headunsafe(and in this casethe C program is proved safe). IfIspdoes not enjoy this property we iterate the specializationprocess with the objective of deriving a CLP program where wecan prove unsafety or safety.During the various specializations we may apply different strategies for propagating information(either propagating forward from an initial configuration,or propagating backward from anerror configuration) and different operators (such as widening and convex hull operators) forgeneralizing predicate definitions. Due to the undecidability of program safety, the iteratedspecialization process may not terminate. By an experimental evaluation carried out on a setof examples taken from the literature, we show that our method is competitive with respect tostate-of-the-art software model checkers.