Verifying programs via iterated specialization

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of C programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from the initial configurations. We encode the interpreter of the language as a CLP program I, and we also encode the safety property to be verified as the negation of a predicate unsafe defined in I. Then, we specialize the CLP program I with respect to the given C program and the given initial and error configurations, with the objective of deriving a new CLP program Isp which either contains the fact unsafe (and in this case the C program is proved unsafe) or contains no clauses with head unsafe (and in this case the C program is proved safe). If Isp does not enjoy this property we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating informatio