| Title: | Program Verification using Constraint Handling Rules and Array Constraint Generalizations |
| Authors: | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti |
| Proceedings: | VPT 2014 EasyChair Proceedings |
| Editors: | Alexei Lisitsa and Andrei Nemytykh |
| Keywords: | Program verification, Program transformation, Constraint logic programming |
| Abstract: | The transformation of constraint logic programs (CLP programs)
has been shown to be an effective methodology
for verifying properties of imperative programs.
By following this methodology, we encode the negation
of a partial correctness property of an imperative
program \textit{prog} as a predicate {\tt incorrect} defined
by a CLP program $P$, and we show that
\textit{prog} is correct by transforming $P$ into
the empty program through the application
of semantics preserving transformation rules.
Some of these rules perform replacements of constraints
that encode properties of the data structures manipulated
by the program \textit{prog}.
In this paper we show that Constraint Handling Rules (CHR)
are a suitable formalism for representing and applying
constraint replacements during the transformation of CLP programs.
In particular, we consider programs that manipulate integer
arrays and we present a CHR encoding of a constraint replacement
strategy based on the theory of arrays.
We also propose a novel generalization strategy for
constraints on integer arrays that combines
the CHR constraint replacement strategy
with various generalization operator for linear constraints,
such as widening and convex hull.
Generalization is controlled by additional constraints
that relate the variable identifiers in the imperative
program and the CLP representation of their values.
The method presented in this paper has been implemented and
we have demonstrated its
effectiveness on a set of
benchmark programs taken from the literature. |
| Pages: | 16 |
| Talk: | Jul 17 11:30 |
| Paper: |  |