Verifying Array Programs by Transforming Verification Conditions

We present a method for verifying properties of imperativeprograms manipulating integer arrays. We assume that we are given aprogram and a property to be verified. Theinterpreter(that is, the op-erational semantics) of the program is specified as a set of Horn clauseswith constraints in the domain of integer arrays, also calledconstraintlogic programs over integer arrays, denoted CLP(Array). Then, by spe-cializing the interpreter with respect to the given program and property,we generate a set ofverification conditions(expressed as a CLP(Array)program) whose satisfiability implies that the program verifies the givenproperty. Our verification method is based on transformations that pre-serve the least model semantics of CLP(Array) programs, and hence thesatisfiability of the verification conditions. In particular, we apply theusual rules for CLP transformation, such as unfolding, folding, and con-straint replacement, tailored to the specific domain of integer arrays. Wepropose an automatic strategy that guides the application of those ruleswith the objective of deriving a new set of verification conditions whichis either trivially satisfiable (because it contains no constrained facts)or is trivially unsatisfiable (because it contains the factfalse). Our ap-proach provides a very rich program verification framework where onecan compose together several verification strategies, each of them beingimplemented by transformations of CLP(Array) programs.