A new style of theorem proving for program checking

Title:A new style of theorem proving for program checking
Speaker: Maria Paola Bonacina (Universita` degli Studi di Verona, Italy) http://profs.sci.univr.it/~bonacina/
Time:10:00am, Thursday, June.9th
Venue:Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract:Applications in software verification require determining the satisfiability of first-order formulae, often with quantifiers, with respect to background theories. Superposition-based inference systems are strong at reasoning with equality, quantifiers, and Horn clauses. Satisfiability modulo theories (SMT) solvers are strong at reasoning with propositional logic, including huge non-Horn clauses, ground equalities and integrated theories such as arithmetic. This talk presents a new style of theorem proving that combines these complementary strengths by integrating superposition tightly in the SMT-solver, in such a way that each engine does what it is best at. The resulting DPLL(Gamma+T) system is refutationally complete and is a decision procedure for several theories and combinations thereof. Its features include model-based theory combination, speculative inferences to obtain decision procedures, and a modular structure that allows us to obtain an interpolation system for DPLL(Gamma+T) from interpolation systems for its components.