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

• Cesare Tinelli (University of Iowa)
• Monday 17 July 2017, 15:30-16:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact INI IT.

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.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.