Decision procedures with unsound theorem proving for software verification

Supervisor
Prof.ssa Maria Paola Bonacina - Dipartimento di Informatica, Universita` degli Studi di Verona
Date and time
Tuesday, May 19, 2009 at 4:15 PM - Ore 16.15 caffè e pasticcini, ore 16.30 inizio seminario
Place
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Maria Paola Bonacina
External reference
Publication date
March 31, 2009
Department
 

Summary

Applications in software verification often require determining
the satisfiability of first-order formulae, including quantifiers,
with respect to some background theories. Superposition-based
inference systems are strong at reasoning with equality,
universally quantified variables, and Horn clauses. Satisfiability
modulo theories (SMT) solvers are strong at reasoning with
propositional logic, including non-Horn clauses, ground equalities
and integrated theories such as linear arithmetic.
This talk presents an approach to combine these complementary strengths
by integrating the superposition-based inference system in the SMT-solver.
Since during software development conjectures are usually false,
it is desirable that the theorem prover terminates on satisfiable
instances. In the integrated approach termination can be enforced
by introducing additional axioms in such a way that the system
detects and recovers from any ensuing unsoundness.

Joint work with Leonardo de Moura and Chris Lynch






© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234