Software Model Checking by Program Specialization

We present a method for performing model checking of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We have considered a simple imperative language, called SIMP, extended with a nondeterministic choice operator, and we have introduced a CLP interpreter which defines the operational semantics of SIMP. Our software model checking method which consists in: (1) translating a given SIMP program, together with the safety property to be verified and a description of the input values, into terms, (2) specializing the CLP interpreter with respect to the above translation, and (3) computing the least model of the specialized interpreter. By inspecting the derived least model we can verify whether or not the given SIMP program satisfies the safety property. The method is fully automatic and has been implemented using the MAP transformation system. We have shown the effectiveness of our method by applying it to some examples taken from the literature and we have compared its performance with that of other state-of-the-art software model checkers.