Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software SMTCoq
SMTCoq - Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
Date of the last release: 01 March 2016

Person in charge : KELLER Chantal


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 and CVC4.

More information: https://smtcoq.github.io/

Software - Licence : CeCILL-C



Research activities

Members

Group
  Verification of Algorithms, Languages and Systems

Software & patents
CODALAB
Codalab

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE