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. 544  (Next)  

Fioravanti F., Alberto Pettorossi, Maurizio Proietti

Verifying CTL properties of infinite state systems by specializing constraint logic programs

ABSTRACT

We propose a method for the specification and the automated verification of temporal properties of infinite state reactive systems. Our method makes use of constraint logic programs (CLP) with locally stratified negation and program specialization. We specify the temporal properties of a reactive system by means of a CLP program whose perfect model consists of all atoms sat(s,varphi) such that state s satisfies property ( varphi ). We verify a temporal property of a system by using a method based on the specialization of the corresponding CLP program w.r.t. the initial states of the system and the given property. Our specialization method makes use of: (i) a set of specialization rules which preserve the perfect model of CLP programs, and (ii) an automatic strategy which guides the application of the rules for making a proof of the property of interest. Our strategy always terminates and it is sound for the verification of properties which are expressible in the CTL branching time logic. Due to the undecidability of CTL for infinite state systems, our strategy is incomplete. However, by using a prototype implementation, we show that it is successful for the verification of several infinite state systems.