Synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software

The goal of this project is to develop a method to prove properties of programs by combining deduction, satisfiability solving and model checking. The project is organized in three main threads:

Synthesis of satisfiability procedures from theorem-proving strategies
Decision procedures for deduction-based model checking of software
Development and assessment of model-checking techniques for software verification

Institutions

People

At the Università degli Studi di Verona:
- Maria Paola Bonacina, Coordinator of the project and head of the project unit in Verona
- Stephan Schulz
- Stefano Ferrari
in cooperation with
- Silvio Ranise, LORIA and INRIA-Lorraine, Nancy
At the Università degli Studi di Genova:
- Alessandro Armando, head of the project unit in Genova
- Claudio Castellini
- Luca Compagna
- Giorgio Delzanno
- Pierre Ganty
- Jacopo Mantovani
At the Università degli Studi di Napoli "Federico II":
- Massimo Benerecetti, head of the project unit in Napoli
in cooperation with
- Luca Spalazzi, Dipartimento di Ingegneria Informatica, Gestionale e dell'Automazione, Università Politecnica delle Marche.

Duration

24 months: November 2003 - November 2005.

Maria Paola Bonacina