-
Notifications
You must be signed in to change notification settings - Fork 1
System veriT
veriT was initially designed by David Déharbe and Pascal Fontaine. Other important contributers were Daniel El Ouraoui, Haniel Barbosa and Hans-Jörg Schurr.
Hans-Jörg Schurr is currently the most involved person in the development.
veriT is an SMT (Satisfiability Modulo Theories) solver. It is proof-producing, and complete for quantifier-free formulas with uninterpreted functions and linear arithmetic on real numbers and integers. It also offers good support for quantifiers.
- Proving
- Model finding
The input format is SMT-LIB 2.6. The language accepted by veriT corresponds to the quantified and unquantified logics with uninterpreted symbols and linear arithmetic.
veriT follows the SMT-LIB reporting standard
The input format is SMT-LIB 2.6.
veriT is used within the Sledgehammer module of Isabelle. veriT's support for proofs, together with a reasonable efficiency, makes it very appropriate in this context.
veriT is also used in the SMT plug-in for Rodin, an Eclipse-based development environment for Event-B. The plug-in allows to use SMT-solvers to discharge proof obligations.
veriT participates to the annual SMT competition SMT-COMP.
veriT is written in C. It is open-source and distributed under the BSD license.
Maintained
Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine. veriT: An Open, Trustable and Efficient SMT-Solver. Proc. of CADE-22, volume 5563 of Lecture Notes in Computer Science, pp. 151-156, 2009. DOI: 10.1007/978-3-642-02959-2_12.