View on GitHub

SMTCoq

Download this project as a .zip file Download this project as a tar.gz file

Presentation

SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:

Installation and use

SMTCoq is freely available on GitHub. It is currently availaible for Coq-8.9 (and native-coq). A release together with an opam package will be available soon.

See the examples to see how to use SMTCoq.

SMTCoq is distributed under the CeCILL-C license.

Example

Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.

Section group.
  Variable e : Z, inv : Z -> Z, op : Z -> Z -> Z.

  Hypothesis associative :
    forall a b c, op a (op b c) = op (op a b) c.
  Hypothesis identity : forall a, (op e a = a).
  Hypothesis inverse : forall a, (op (inv a) a = e).

  Add_lemmas associative identity inverse.

  Lemma identity' :
    forall a, (op a e = a).
  Proof. smt. Qed.

  Lemma inverse' :
    forall a, (op a (inv a) = e).
  Proof. smt. Qed.

  Lemma unique_identity e':
    (forall z, op e' z = z) -> e' = e.
  Proof. intros pe'; smt pe'. Qed.

  Clear_lemmas.
End group.

People

Current team

Past contributors

Publications

Reference

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.

Other publications

  1. 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.
  2. 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.
  3. 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.
  4. SMTCoq : automatisation expressive et extensible dans Coq, Blot, Valentin; Bousalem, Amina; Garchery, Quentin; Keller, Chantal, JFLA - Journées Francophones des Langages Applicatifs - 2019.

Talk

Overview of SMTCoq (February, 2019)