Abstract

This talk will give an overview of SMT Coq, 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, SMT Coq 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 SMT Coq 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 SMT Coq'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.