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: Conference
• Year: 2009
• Where: CADE
• Authors: David Déharbe, Diego Caminha B. de Oliveira, Pascal Fontaine, Thomas Bouton
• Keywords: Automated Reasoning, CADE 2009, Difference Logic, Real Numbers, Satisfiability Modulo Theory