An open, trustable and efficient SMT-solver
veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source, 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. The input format is the SMT-LIB 2.0 language and DIMACS.
veriT is open-source and distributed under the BSD license.
veriT has proof-production capabilities that may be used or checked by external tools. At the SMT competition veriT's performance is competitive for some theories.
The project is under active development, and newcomers are most welcome! Just contact us.
Founder and Lead Developer
Professor at Université de Liège
in Belgium
(Montefiore Institute).
Lead Developer
PhD student at
Inria Nancy Grand Est
and Université de Lorraine in
Nancy, France
Developer
Assistant professor at Universidade Federal de Minas Gerais
(UFMG) in Belo Horizonte, Brazil.
Past developers have helped a lot:
Special thanks to:
In case you want to participate in the development of a SMT-solver, you may want to join the team of developers of veriT.
If you are interested in a PhD or post-doctoral position to work on the development and applications of veriT, either at LORIA (Nancy, France) or ULiège (Liège, Belgium), please contact us in advance so that we look for funding for your stay.
The SMT-LIB standard provides a common input/output language for SMT solvers. veriT follows the SMT-LIB standard for the features it supports. The language is based on s-expressions and mostly designed to be easy to parse. A multi-sorted first order logic serves as the semantic. We are also involved in the development of the standard.
The SMT-LIB initiative also maintains a big collection of SMT-LIB benchmarks. Those benchmarks provide an invaluable resource for the development and testing of veriT. We strongly encourage users of SMT solvers to submit benchmarks to the SMT-LIB project.
Isabelle/HOL can call veriT to discharge proof goals. This is implemented as part of the smt tactic and complements the existing support for the SMT solver Z3. The method reconstructs the proofs generated by veriT inside the trusted kernel of Isabelle/HOL.
Furthermore, veriT is available as a backend to the Sledgehammer tool to find proofs and it will also suggest the veriT powered smt method to the user as a command to insert into their proof script.
The GridTPT platform has been used to support the development of the SMT solver veriT for several years. Since programming provers is a complex task, a good testing platform can contribute in detecting bugs early and helping development. GridTPT's features are fairly standard, but it allows to easily distribute the task in a cluster for extensive tests to be completed quickly.
GridTPT is neither stable nor easy to use, but if you are looking for a testing platform for your prover or solver, contact us and we will help you to install, configure and use the solver. This will also help us to improve the tool and hopefully eventually distribute a adaptable tool to the community. The code is BSD and written mostly in Python.
Interface between the veriT SAT solver and either Matlab or Octave. The SAT problem can be modeled using Matlab matrices. The current implementation allows to either use dense or sparse matrices. It has already been used successfully under Windows 7 64 bits and Ubuntu 13.10 64 bits. It is intended to be used by industrial as well as academic communities. The code is released under the BSD license.
Different packages for different operating systems and architectures are available:
The GNU Multiple Precision Arithmetic Library is used to represent and manipulate numerical value. It is distributed under the GNU LGPL.
Rodin is an Eclipse-based development environment for Event-B. The SMT plug-in for Rodin allows to use SMT-solvers to discharge proof obligations. It is still under development.
REDUCE is a computer algebra system often used as an algebraic calculator for problems that are possible to do by hand. Some versions of veriT use Reduce.
The E equational theorem prover is a first-order logic theorem prover based on the superposition calculus. It was used by veriT as a standalone application. It is released under the GNU GPL.
CRefine is an editor that supports the formal development of concurrent object-oriented software in Circus by implementing a refinement calculus.
Bliss is a backtracking algorithm for computing automorphism groups and canonical forms of graphs, based on individualization and refinement.
Saucy is the implementation of a symmetry-discovery algorithm.
PermLib is a C++ library for permutation computations.
In early releases, veriT used the SAT-solver MiniSat to represent and manipulate the boolean structure of the formulas.
For questions, comments, feature requests and bug reports, please .
While reporting bugs, please make sure you give enough information in your report to enable us to reproduce and fix the problem:
Thanks for helping us improving veriT.
