This page shows all publications that appeared in the IASI annual research reports. Authors currently affiliated with the Institute are always listed with the full name.

You can browse through them using either the links of the following line or those associated with author names.

Show all publications of the year  2014, with author Pettorossi A., in the category IASI Research Reports (or show them all):

---

IASI Research Report n. 14-07    

Emanuele De Angelis, Fioravanti F., Pettorossi A., Maurizio Proietti

A Rule-based Verification Strategy for Array Manipulating Programs

ABSTRACT

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 {pre} prog {post} defining 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 manipulating array constraints, and also applies suitable combinations of widening and convex hull operators for generalizing 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.