SMTCoq is a plugin for the Coq interactive theorem prover to work in conjunction with automated theorem provers based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), in an efficient and expressive way. First, it allows one to formally establish, in a proof assistant, mathematical results relying on large combinatorial properties that require automatic Boolean reasoning. Second, it provides a new Coq decision procedure that can be seen as a combination of existing decision procedures.

To achieve this objective with the same degree of safety as Coq itself, SMTCoq communicates with SAT and SMT solvers that, in addition to a yes/no answer, can output traces of their internal proof search. The heart of SMTCoq is thus a certified, efficient and modular checker for such traces expressed in a format that can encompass most aspects of SMT reasoning. Preprocessors - that need not be certified - for proof traces coming from the state-of-the-art SMT solvers CVC4 and veriT and SAT solver zChaff are implemented.

In this talk, I will present the general ideas behind SMTCoq, and focus on the recent features, in particular the treatment of quantifiers.