University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins .

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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 that 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 tame the proofs’ complexity and to be extendable. It can currently check witnesses from the SAT solver zChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq’s logic by calling external provers and carefully checking their answers.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Spanish & Portuguese Webinar & LT2, Computer Laboratory, William Gates Building. Talks related to atmosphere and ocean dynamics and climate science

Other talks

Tea and Coffee Break Packing the Border: Quail Crates and the Regulation of Animal Movement on the US-Mexico Border, 1910s-1940s Reproducibility In Astrophysical Simulations: The AGORA Initiative and a 14-Year Human Experiment (In Memory of Joel Primack) Group Work Welcome Reception and Poster Session Title to be confirmed
 

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