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 Fioravanti F., in the category IASI Research Reports (or show them all):

---

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

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

Automated Verification of Relational Program Properties

ABSTRACT

We present a method for verifying relational program prop- erties, that is, properties that relate the input and the output of two programs. Our verification method is parametric with respect to the definition of the semantics of the programming language in which the programs are written. That definition consists of a set Int of constrained Horn clauses (CHC) that encode the interpreter of the programming language. Then, given the programs and the relational property we want to verify, we generate, by using Int, a set of constrained Horn clauses whose satisfiability is equivalent to the validity of the property. Unfortu- nately, state-of-the-art solvers for CHC have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We pro- pose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these trans- formations, based on unfolding and folding rules, preserve satisfiability. Through an experimental evaluation we show that in many cases CHC solvers are able to prove the (un)satisfiability of sets of clauses obtained by applying the transformations we propose, whereas the same solvers are unable to perform those proofs when given as input the original sets of constrained Horn clauses.