University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq

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

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact info@newton.ac.uk.

BPR - Big proof

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.



This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity