Decision procedures with unsound theorem proving for software verification

Relatore
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
Luogo
Ca' Vignal - Piramide, Piano 0, Sala Verde
Referente
Maria Paola Bonacina
Referente esterno
Data pubblicazione
31 marzo 2009
Dipartimento
 

Riassunto

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  Università degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234