Verification of Imperative Programs by Constraint Logic Program Transformation

Emanuele De Angelis
(DEC, University `G. D'Annunzio', Pescara, Italy)
Fabio Fioravanti
(DEC, University `G. D'Annunzio', Pescara, Italy)
Alberto Pettorossi
(DICII, University of Rome Tor Vergata, Rome, Italy)
Maurizio Proietti
(IASI-CNR, Rome, Italy)

We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this case prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation.

In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (Festschrift for Dave Schmidt), Manhattan, Kansas, USA, 19-20th September 2013, Electronic Proceedings in Theoretical Computer Science 129, pp. 186–210.
Published: 19th September 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: