SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:
- a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
- decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination.
Installation and use
SMTCoq is distributed under the CeCILL-C license.
If you have any question or remark, you are invited to join the SMTCoq forum.
Bugs can be reported on github.
Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.
From SMTCoq Require Import SMTCoq. Section Group. Variable G : Type. (* We suppose that G has a decidable equality *) Variable HG : CompDec G. Variable op : G -> G -> G. Variable inv : G -> G. Variable e : G. Local Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60). (* We can prove automatically that we have a group if we only have the "left" versions of the axioms of a group *) Hypothesis associative : forall a b c : G, op a (op b c) ==? op (op a b) c. Hypothesis inverse : forall a : G, op (inv a) a ==? e. Hypothesis identity : forall a : G, op e a ==? a. Add_lemmas associative inverse identity. Lemma inverse' : forall a : G, op a (inv a) ==? e. Proof. smt. Qed. Lemma identity' : forall a : G, op a e ==? a. Proof. smt inverse'. Qed. Lemma unique_identity e': (forall z, op e' z ==? z) -> e' ==? e. Proof. intros pe'; smt pe'. Qed. Clear_lemmas. End Group.
Want to participate?
SMTCoq is an ambitious, collaborative project: everyone is welcome! There are many and varied enhancement to do: join the SMTCoq forum to discuss!
- Clark Barrett (Stanford University)
- Valentin Blot (Inria Saclay - Île-de-France)
- Boris Djalal (Inria Saclay - Île-de-France)
- Louise Dubois-de-Prisque (Inria Saclay - Île-de-France)
- Burak Ekici (The University of Iowa)
- Quentin Garchery (Université Paris-Sud, Inria Saclay - Île-de-France)
- Benjamin Grégoire (Inria Sophia Antipolis)
- Guy Katz (Stanford University)
- Chantal Keller (Université Paris-Sud)
- Alain Mebsout (OcamlPro)
- Andrew Reynolds (The University of Iowa)
- Laurent Théry (Inria Sophia Antipolis)
- Cesare Tinelli (The University of Iowa)
- Pierre Vial (Inria Saclay - Île-de-France)
- Mikaël Armand (Inria Sophia Antipolis)
- Amina Bousalem (Université Paris-Sud)
- Germain Faure (Inria Saclay)
- Tianyi Liang (The University of Iowa)
- Benjamin Werner (École polytechnique)
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin, CPP - Certified Programs and Proofs - First International Conference - 2011.
- SMTCoq: A plug-in for integrating SMT solvers into Coq (Tool Paper), Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark, CAV - International Conference on Computer Aided Verification - 2017.
- Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew; Tinelli, Cesare, HaTT - on Hammers for Type Theories - First International Workshop - 2016.
- Verifying SAT and SMT in Coq for a fully automated decision procedure, Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin, PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories - 2011.
- SMTCoq : automatisation expressive et extensible dans Coq, Blot, Valentin; Bousalem, Amina; Garchery, Quentin; Keller, Chantal, JFLA - Journées Francophones des Langages Applicatifs - 2019.