Verification of Imperative Programs by Constraint Logic Program Transformation

We present a method for verifying partial correctness properties of imperative programs that ma-nipulate integers and arrays by using techniques based on the transformation of constraint logicprograms (CLP). We use CLP as a metalanguage for representing imperative programs, their execu-tions, and their properties. First, we encode the correctness of an imperative program, sayprog, asthe negation of a predicateincorrectdefined by a CLP programT. By construction,incorrectholds in the least model ofTif and only if the execution ofprogfrom an initial configuration eventu-ally halts in an error configuration. Then, we apply to programTa sequence of transformations thatpreserve its least model semantics. These transformationsare based on well-known transformationrules, such asunfoldingandfolding, guided by suitable transformationstrategies, such asspecializa-tionandgeneralization. The objective of the transformations is to derive a new CLP programTransfTwhere the predicateincorrectis defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this caseprogis correct). In the case wherewe derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since theproblem is undecidable, this process may not terminate. We show through examples that our methodcan be applied in a rather systematic way, and is amenable to automation by transferring to the fieldof program verification many techniques developed in the field of program transformation.