Integrating automated reasoning in model checking:
towards push-button formal verification of large-scale and
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
24 months: September 2008 - September 2010.
Maria Paola Bonacina