Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems - Design and integration of proof engines for program analysis

Starting date
September 22, 2008
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Bonacina Maria Paola
URL
http://profs.sci.univr.it/~bonacina/prin2007.html
Keyword
Automated reasoning; program analysis; decision procedures for satisfiability modulo theories; rewrite-based theorem proving; automated model building

Since computer software is everywhere, the economic impact of software errors cannot be overestimated. The cost of errors could be significantly reduced by techniques that enable earlier and more effective identification and removal of defects. The importance of the problem demands to investigate fully automated techniques. The successes of model checking in hardware and protocol verification suggest to investigate software model checking. However, software model checking is considerably harder, because software involves infinite state systems. Complexity is attacked by abstraction: if a piece of software is too complex, an abstract version that is simpler than the original is analyzed. However, an error detected in the abstract model is not necessarily an error in the concrete program. In order to bridge this gap, model checking needs automated reasoning. The correspondence between an error in the model and an error in the concrete program is reduced to a satisfiability problem, whose proof can be used to refine the abstraction, if it turns out that a spurious error was detected. The thrust of this project is to define, design and implement efficient, scalable and expressive decision procedures for satisfiability.

Sponsors:

Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Research areas involved in the project
Sistemi intelligenti
Artificial intelligence
Publications
Title Authors Year
Interpolation systems for ground proofs in automated deduction: a survey Maria Paola Bonacina; Moa Johansson 2015
On interpolation in automated theorem proving Maria Paola Bonacina; Moa Johansson 2015
Canonical ground Horn theories Maria Paola Bonacina; Nachum Dershowitz 2013
On deciding satisfiability by theorem proving with speculative inferences Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura 2011
On interpolation in decision procedures Bonacina, Maria Paola; Moa, Johansson 2011
Towards interpolation in an SMT solver with integrated superposition Maria Paola Bonacina; Moa Johansson 2011
On theorem proving for program checking - Historical perspective and recent developments Bonacina, Maria Paola 2010
Theory decision by decomposition Maria Paola Bonacina; Mnacho Echenim 2010
On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving Maria Paola Bonacina; Christopher A. Lynch; Leonardo de Moura 2009

Activities

Research facilities