Verifying Array Programs by Transforming Verification Conditions

We present a method for verifying properties of imperative programs manipulating integer arrays. We assume that we are given a program and a property to be verified. The {\em interpreter} (that is, the operational semantics) of the program is specified as a set of Horn clauses with constraints in the domain of integer arrays, also called {\em constraint logic programs over integer arrays}, denoted CLP(Array). Then, by specializing the interpreter with respect to the given program and property, we generate a set of {\em verification conditions} (expressed as a CLP(Array) program) whose satisfiability implies that the program verifies the given property. Our verification method is based on transformations that preserve the least model semantics of CLP(Array) programs, and hence the satisfiability of the verification conditions. In particular, we apply the usual rules for CLP transformation, such as unfolding, folding, and constraint replacement, tailored to the specific domain of integer arrays. We propose an automatic strategy that guides the application of those rules with the objective of deriving a new set of verification conditions which is either trivially satisfiable (because it contains no constrained facts) or is trivially unsatisfiable (because it contains the fact \textit{false}). Our approach provides a very rich program verification framework where one can compose together several verification strategies, each of them being implemented by transformations of CLP(Array) programs.