salle A. Turing CE4
30 mai 2013 - 14h00
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
par Chantal Keller de Laboratoire d'informatique de l'X
Abstract: In this talk, I will present a way to enjoy the power of SAT and SMT
provers in Coq without compromising soundness. This requires these
provers to return not only a yes/no answer, but also a proof witness
that can be independently rechecked. We present such a checker, written
and fully certified in Coq. It is conceived in a modular way, in order
to tame the proofs' complexity and to be extendable. It can currently
check witnesses from the SAT solver zChaff and from the SMT solver
veriT. Experiments highlight the efficiency of this checker. On top of
it, new reflexive Coq tactics have been built that can decide a subset
of Coq's logic by calling external provers and carefully checking their
answers.
