Integrating SAT, QBF and SMT Solvers
with Interactive Theorem Provers
- Speaker
Tjark Weber, Cambridge
- Date and Time
Wednesday, September 14th, 2011 at 10:15
- Location
Polacksbacken, room 1145
- Abstract
-
Interactive Theorem Provers (ITPs) are redefining our notion of formal proof and the way mathematics and program verification are being carried out. Improved automation in ITPs leads to increased productivity, thereby enabling new and large-scale applications. At the same time, LCF-style ITPs, which are based on relatively small trusted kernels, provide high correctness assurances.
In this talk, I will give an overview of working integrations of SAT, QBF and SMT solvers with interactive theorem provers Isabelle and HOL4. These integrations do not need to be trusted: the external solvers generate certificates that are checked by the ITPs' kernels. Evaluation on large benchmark collections shows that LCF-style certificate checking is feasible even for proofs with millions of inferences.
I will also briefly discuss some applications that have benefited from these integrations already: in particular an Isabelle/HOL repository of algebraic structures that form a basis for various software development methods, and a formalization of the C++11 concurrency memory model.