skip to content

SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq

Presented by: 
Cesare Tinelli
Monday 17th July 2017 - 15:30 to 16:00
INI Seminar Room 2
This talk will give an overview of SMTCoq, a plug-in for the integration of external solvers into the Coq proof assistant. Based on a checker for general first-order proof certificates fully implemented and proved correct in Coq, SMTCoq has two main functionalities: (i) act as a trustworthy checker for proof certificates produced by SAT or SMT solvers, (ii) increase the level of automation in Coq by dispatching selected Coq subgoals to such solvers and incorporating their proof, all in a safe way. The current version of SMTCoq supports proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols.The talk will discuss SMTCoq's philosophy and architecture, and will provide some technical details on the integration of CVC4 as well as examples of automated goal discharging based on combined calls to CVC4 and veriT.The talk is based on joint work with Burak Ekici, Alain Mebsout, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons