Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel SMTCoq
SMTCoq - Plug-in de communication entre Coq et prouveurs externes
Date de dernière version : 01 mars 2016

Responsable : 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.

Pour en savoir plus: https://smtcoq.github.io/

Logiciel - Licence : CeCILL-C



Activités de recherche

Membres

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Logiciels et brevets
DNADNA
Deep Neural Networks for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas