Decision procedures with unsound theorem proving for software verification

Speaker:  Prof.ssa Maria Paola Bonacina - Dipartimento di Informatica, Universita` degli Studi di Verona
  Tuesday, May 19, 2009 at 4:15 PM Ore 16.15 caffè e pasticcini, ore 16.30 inizio seminario

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


Place
Ca' Vignal - Piramide, Floor 0, Hall Verde

Programme Director
Maria Paola Bonacina

External reference
Publication date
March 31, 2009

Studying

Share