ISTITUTO DIANALISI DEISISTEMI ED INFORMATICA CONSIGLIO NAZIONALE DELLE RICERCHE

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 fpreg prog fpostg dening a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect dened by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program veri cation 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 i it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satises 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 strateg