Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems

This project aims at contributing to the development of new model-checking techniques for data-intensive software and industrial-scale hardware designs. The adopted model-checking framework is counter-example guided abstraction refinement. A key ingredient will be automated reasoning procedures to decide the formulae generated by the SW/HW verification problem. The project is organized in four main threads:

Design and integration of proof engines for program analysis
Model checking, decision procedures and automatic tool configuration for the formal verification of software
Integration of abstraction in model checking for the verification of infinite-state and open systems
New efficient procedures for satisfiability modulo theories and their application to the formal verification of complex systems

Institutions

People

At the Università degli Studi di Verona:
- Maria Paola Bonacina, Head of the project unit in Verona
- Moa Johansson, Postdoc fellow from October 1st 2009 through September 30th 2011
At the Università degli Studi di Genova:
- Alessandro Armando, Coordinator of the project and head of the project unit in Genova
At the Università degli Studi di Napoli "Federico II":
- Massimo Benerecetti, Head of the project unit in Napoli
At the Università degli Studi di Trento:
- Roberto Sebastiani, Head of the project unit in Trento

Duration

24 months: September 2008 - September 2010.

Maria Paola Bonacina