A Rule-based Verification Strategy for Array Manipulating Programs

We present a method for verifying properties of imperative programs that manipulate
integer arrays. Imperative programs and their properties are represented by using Constraint Logic
Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ} prog {ψ}
that defines a partial correctness property of an imperative program prog, we encode the negation
of the property as a predicate incorrect defined by a CLP program P, and we show that the
property holds by proving that incorrect is not a consequence of P. Program verification is
performed by applying a sequence of semantics preserving transformation rules and deriving a new
CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The
rules are applied according to an automatic strategy whose objective is to derive a program T that
satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that
incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving
that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory
of arrays for the manipulation of array constraints, and also applies the widening and convex hull
operators for the generalization of linear integer constraints. The strategy has been implemented in
the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set
of benchmark array programs taken from the literature