Publications of Maurizio Proietti

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  ALL, with author Proietti M., in the category IASI Research Reports (or show them all):


IASI Research Report n. 14-07  (Previous    Next)  

Emanuele De Angelis, Fioravanti F., Alberto Pettorossi, 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.
back
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -