Breaking News

veriT received the Gold Medal at the VSL Olympic Games 2014 for SMT!

veriT was declared the overall winner of the 2014 SMT competition, held as part of the VSL Olympic Games. The results of the competition are available on the Web site.

The success of the different solvers was measured as a combination of the number of benchmark problems solved in the various categories, the number of erroneous answers, and the time taken. Solvers that produced erroneous answers for certain benchmark categories were at a strong disadvantage for the overall score. When appreciating the results, please be aware that any particular metric combining multiple criteria is somewhat arbitrary. As shown on the bottom of the result Web page, a different scoring of the results would have led to a different ranking of the participating solvers. Moreover, the competition runs versions of the solvers that may be different from the stable versions distributed through their respective Web sites.

Distinguishing features of the veriT solver are reasonable efficiency, proof production, small code size, and a very open license.

What is veriT?


veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.

The input format is the SMT-LIB language (both versions 1.2 and 2.0) and DIMACS, but veriT can also be used as a standalone library and incorporated in third-party software. The tool is open-source and distributed under the BSD license.

veriT is complete for the logic of unquantified formulas over uninterpreted symbols, difference logic over integers and real numbers, and the combination thereof. This corresponds to the logics identified as QF_IDL, QF_RDL, QF_UF and QF_UFIDL in the SMT-LIB benchmarks. veriT includes quantifier reasoning capabilities through quantifier instantiation heuristics and the integration of a first-order prover and linear arithmetics for integers and real numbers.

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 ancestor of veriT is haRVey. Its web page can still be reached here.

How to contribute?


veriT is under heavy development, and newcomers to the project are most welcome! Check the Job section of this site, and contact us.