veriT: an open, trustable and efficient SMT-solver

Abstract : This article describes the first public version of the satisfiability modulo theory (SMT) solver {\verit}. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.
Type de document :
Communication dans un congrès
Renate A. Schmidt. 22nd International Conference on Automated Deduction - CADE 22, Aug 2009, Montreal, Canada. Springer Berlin / Heidelberg, 5663, pp.151-156, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02959-2_12〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00430634
Contributeur : Pascal Fontaine <>
Soumis le : lundi 9 novembre 2009 - 12:49:28
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

Identifiants

Collections

Citation

Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver. Renate A. Schmidt. 22nd International Conference on Automated Deduction - CADE 22, Aug 2009, Montreal, Canada. Springer Berlin / Heidelberg, 5663, pp.151-156, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02959-2_12〉. 〈inria-00430634〉

Partager

Métriques

Consultations de la notice

117