Decision procedures with unsound theorem proving for software verification

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