BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Modular Integration of SAT/SMT Solvers to Coq through Proof Witn
 esses - Chantal Keller
DTSTART:20140624T090000Z
DTEND:20140624T100000Z
UID:TALK53083@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In this talk\, I will present a way to enjoy the power of SAT 
 and SMT provers in Coq without compromising soundness. This requires these
  provers to return not only a yes/no answer\, but also a proof witness tha
 t can be independently rechecked. We present such a checker\, written and 
 fully certified in Coq. It is conceived in a modular way\, in order to tam
 e the proofs' complexity and to be extendable. It can currently check witn
 esses from the SAT solver zChaff and from the SMT solver veriT. Experiment
 s highlight the efficiency of this checker. On top of it\, new reflexive C
 oq tactics have been built that can decide a subset of Coq's logic by call
 ing external provers and carefully checking their answers.
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR