Decision procedures with unsound theorem proving for software verification

Prof.ssa Maria Paola Bonacina - Dipartimento di Informatica, Universita` degli Studi di Verona

Data e ora
martedì 19 maggio 2009 alle ore 16.15 - Ore 16.15 caffè e pasticcini, ore 16.30 inizio seminario

Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Maria Paola Bonacina

Data pubblicazione
31 marzo 2009



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

Offerta formativa