Write a Blog >>
Sat 25 Jan 2020 09:00 - 10:00 at Maurepas - Invited Talk Chair(s): Robbert Krebbers

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.

SMTCoq: safe and efficient automation in Coq (smtcoq.pdf)407KiB

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited TalkCoqPL at Maurepas
Chair(s): Robbert Krebbers Delft University of Technology
SMTCoq: Safe and efficient automation in Coq (Keynote)
Chantal Keller LRI, Université Paris-Sud
File Attached