Specialization with Constrained Generalization for Software Model Checking

We present a method for verifying properties of imperativeprograms by using techniques based on constraint logic programming(CLP). We consider a simple imperative language, called SIMP, extendedwith a nondeterministic choice operator and we address the problem ofchecking whether or not asafetyproperty?(that specifies that anunsafeconfiguration cannot be reached) holds for a SIMP programP.Theop-erational semantics of the language SIMP is specified via an interpreterIwritten as a CLP program. The first phase of our verification methodconsists in specializingIwith respect toP, thereby deriving a specializedinterpreterIP. Then, we specializeIPwith respect to the property?andthe input values ofP, with the aim of deriving, if possible, a programwhose least model is a finite set of constrained facts. To this purpose weintroduce a novel generalization strategy which, during specialization,has the objecting of preserving the so called branching behaviour of thepredicate definitions. We have fully automated our method and we havemade its experimental evaluation on some examples taken from the liter-ature. The evaluation shows that our method is competitive with respectto state-of-the-art software model checkers.