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, but veriT is intend also to be used as a standalone library and incorporated in third-party software.
veriT is open-source and distributed under the BSD license.
veriT has proof-production capabilities that may be used or checked by external tools. Although not (yet) as fast as the solvers performing best in the SMT competition, veriT has a decent efficiency.
The project is under heavy development, and newcomers are most welcome! Just contact us.
The tool was updated for SMT-LIB 2.0. Please note that this version of the tool does not support the full syntax but only the features supported by the original tool. E.g. there is no support for quantifiers, or push and pop.
Alternatively, the beta version of another (new) delta debugger developed by Aina Niemetz at the Institute for Formal Models and Verification at Linz University and supporting SMT-LIB syntax version 2.0 is available here.
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.
SMTpp is a tool operating both as a source-to-source transformer and analyzer for SMT-LIB. Our goal is to offer a platform to develop:
SMTpp has grown out of veriT and is available under the ISC license. Check out our GitHub page for more detailed information.
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.
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.
Past developers have helped a lot:
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 post-doctoral position to work on the development and applications of veriT, either at LORIA (Nancy, France) or UFRN (Natal, Brazil), please contact us in advance so that we can obtain funding for your stay.
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.