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-09  (Previous )  

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

Proving Horn Clause Specifications of Imperative Programs

ABSTRACT

We present a method for verifying the correctness of an imperative program with respect to a specification defined in terms of a set of possibly recursive Horn clauses. Given a program prog, we consider a partial correctness specification of the form {phi} prog {psi}, where the assertions phi and psi are predicates defined by a set Spec of Horn clauses. The verification method consists in: (i) encoding the function computed by the program prog (according to the semantics of the imperative language) as a set OpSem of clauses, and then (ii) constructing a set PC of Horn clauses and a predicate p such that if p is false in the least model of PC, that is, M(PC) 6|= p, then {phi} prog {psi} is valid. We also present an extension of the verification method for showing total correctness of programs. Then we present a general proof technique based on unfold/fold transformations of Horn clauses, for checking whether or not M(PC) |= p holds. We also outline a strategy for guiding the application of the unfold/fold transformation rules and performing correctness proofs in an automatic way. Finally, we show some experimental results based on a preliminary implementation of our method.