Verification of Imperative Programs by Transforming Constraint Logic Programs

We present a method for verifying partial correctness prop-erties of imperative programs that manipulate integers and arrays byusing techniques based on the transformation of constraint logic pro-grams (CLP). We use CLP as a metalanguage for representing imper-ative programs, their executions, and their properties. First, we encodethe correctness of an imperative program, sayprog, as the negation ofa predicateincorrectdefined by a CLP programT. By construction,incorrectholds in the least model ofTif and only if the execution ofprogfrom an initial configuration eventually halts in an error configura-tion. Then, we apply to programTa sequence of transformations thatpreserve its least model semantics. These transformations are based onwell-known transformationrules, such asunfoldingandfolding, guidedby suitable transformationstrategies, such asspecializationandgener-alization. The objective of the transformations is to derive a new CLPprogramTransfTwhere the predicateincorrectis defined either by (i)the fact 'incorrect.' (and in this caseprogisnotcorrect), or by (ii)the empty set of clauses (and in this caseprogis correct). In the casewhere we derive a CLP program such that neither (i) nor (ii) holds, weiterate the transformation. Since the problem is undecidable, this pro-cess may not terminate. We show through examples that our methodcan be applied in a rather systematic way, and is amenable to automa-tion by transferring to the field of program verification many techniquesdeveloped in the field of program transformation.