veriT: an open, trustable and efficient SMT-solver

Thomas Bouton; Diego Caminha B. De Oliveira; David Déharbe; Pascal Fontaine

inria-00430634, version 1

veriT: an open, trustable and efficient SMT-solver

Thomas Bouton ¹, Diego Caminha B. De Oliveira ¹, David Déharbe ², Pascal Fontaine () ¹

22nd International Conference on Automated Deduction - CADE 22 5663 (2009) 151-156

Résumé : 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.

1 : MOSEL (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : Universidade Federal de Rio Grande do Norte (UFRN)
Universidade Federal de Rio Grande do Norte

inria-00430634, version 1
http://hal.inria.fr/inria-00430634
oai:hal.inria.fr:inria-00430634
Contributeur : Pascal Fontaine <>
Soumis le : Lundi 9 Novembre 2009, 12:49:28
Dernière modification le : Lundi 23 Novembre 2009, 12:23:12

Voir la fiche détaillée

Documents associés

DOI : 10.1007/978-3-642-02959-2_12

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00430634"><analytic>
<author><persName><forename>Thomas</forename><surname>Bouton</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Diego</forename><surname>Caminha B. De Oliveira</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Déharbe</surname></persName>
<affiliation>
<orgName type="laboratory">UFRN</orgName>
<orgName type="team">Universidade Federal de Rio Grande do Norte</orgName>
<country>BR</country>
<orgName type="institution">Universidade Federal de Rio Grande do Norte</orgName>
</affiliation>
</author>
<author><persName><forename>Pascal</forename><surname>Fontaine</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">veriT: an open, trustable and efficient SMT-solver</title></analytic><monogr><meeting>22nd International Conference on Automated Deduction - CADE 22</meeting><imprint><publisher>Springer Berlin / Heidelberg</publisher><pubPlace><settlement>Montreal</settlement><country>Canada</country></pubPlace><biblScope type="publicationDate">2009-00-00</biblScope><biblScope type="vol">5663</biblScope><biblScope type="pp">151-156</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-02959-2_12</idno><idno type="HALid">http://hal.inria.fr/inria-00430634</idno></biblStruct>
</listBibl>
</listBibl>