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. 12-22  (Previous    Next)  

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

Verifying Programs via Iterated Specialization

ABSTRACT

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of C programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from the initial configurations. We encode the interpreter of the language as a CLP program I, and we also encode the safety property to be verified as the negation of a predicate unsafe defined in I. Then, we specialize the CLP program I with respect to the given C program and the given initial and error configurations, with the objective of deriving a new CLP program I_sp which either contains the fact unsafe (and in this case the C program is proved unsafe) or contains no clauses with head unsafe (and in this case the C program is proved safe). If I_sp does not enjoy this property we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating information (either propagating forward from an initial configuration, or propagating backward from an error configuration) and different operators (such as widening and convex hull operators) for generalizing predicate definitions. Due to the undecidability of program safety, the iterated specialization process may not terminate. By an experimental evaluation carried out on a set of examples taken from the literature, we show that our method is competitive with respect to state-of-the-art software model checkers.