BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:SMTCoq\, a plug-in for the trustworthy integration of SAT/SMT solv
 ers into Coq - Cesare Tinelli (University of Iowa)
DTSTART:20170717T143000Z
DTEND:20170717T150000Z
UID:TALK73321@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION: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 c
 hecker for general first-order proof certificates fully implemented and pr
 oved correct in Coq\, SMTCoq has two main functionalities: (i) act as a tr
 ustworthy checker for proof certificates produced by SAT or SMT solvers\, 
 (ii) increase the level of automation in Coq by dispatching selected Coq s
 ubgoals 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 a
 nd 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&#39\;s philosophy and architecture\, and will provide some technical d
 etails on the integration of CVC4 as well as examples of automated goal di
 scharging based on combined calls to CVC4 and veriT.The talk is based on j
 oint work with Burak Ekici\, Alain Mebsout\, Chantal Keller\, Guy Katz\, A
 ndrew Reynolds\, and Clark Barrett.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR