Program Transformation for Program Verification

We present a transformational approach to program verification and software model checking that uses three main ingredients: (i) Constraint Logic Programming (CLP), (ii) metaprogram-ming and program specialization, and (iii) proof by transformation. (i) Constraints are used for representing in a compact way (finite or infinite) sets of values or memory states, and logic is used for expressing properties of program executions [2, 4, 5]. The least fixpoint semantics and negation allow us to denote both the least models and the greatest models of programs, and thus to reason about the (finite or infinite) behaviour of programs. (ii) Metaprogramming is used for getting a verification technique which is parametric with respect to the programming language in use. In particular, we introduce a CLP program I which defines the (meta)interpreter of the programming language in which the program P to be verified is written. Then, in order to gain efficiency, we remove this interpretation layer by specializing the interpreter I with respect to the given program P [1, 6, 7]. The property ϕ that should be proved (or disproved) about program P, is expressed through the CLP clauses that characterize the set of states in which ϕ holds (or does not hold, respectively). (iii) Having derived a CLP program P ̃ whose semantics represents the behaviour of the given program P and the property ϕ to be verified, we star