veriT's big logo
An open, trustable and efficient SMT-prover

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 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.

Documentation

Here you can find published papers about veriT.

2017

  • Language and proofs for higher-order SMT (work in progress)
    Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. 5th Workshop on Proof eXchange for Theorem Proving (PxTP) co-located with FroCoS, 2017.
    [ pdf | slides ]
  • New techniques for instantiation and proof production in SMT solving
    Haniel Barbosa. Ph.D. thesis. Inria, Université de Lorraine, UFRN. September 2017
    [ pdf | pdf + extended abstracts in fr and pt-br | slides | bibtex ]
  • Subtropical satisfiability
    Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm and Xuan Tung Vu. FroCoS 2017.
    [ pdf | slides | bibtex ]
  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. CADE 2017.
    [ pdf | slides | bibtex | report ]
  • Congruence closure with free variables
    Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. TACAS 2017.
    [ pdf | slides | bibtex | report ]

2016

  • Efficient Instantiation Techniques in SMT (Work in Progress)
    Haniel Barbosa. Workshop on Practical Aspects of Automated Reasoning (PAAR) co-located with IJCAR, 2016.
    [ pdf | bibtex]

2015

  • Adapting Real Quantifier Elimination Methods for Conflict Set Computation.
    Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine. FroCoS 2015.
    [ pdf | bibtex]
  • SMTpp : preprocessors and analyzers for SMT-LIB
    Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine. 13th International Workshop on Satisfiability Modulo Theories (SMT), 2015.
    [ pdf | bibtex]
  • Haniel Barbosa, Pascal Fontaine. Congruence Closure with Free Variables (Work in Progress). 2nd International Workshop on Quantification, (QUANTIFY), 2015.
    [ pdf | bibtex]

2014

  • Extending SMT-LIB v2 with λ-Terms and Polymorphism
    Richard Bonichon, David Déharbe, Cláudia Tavares. Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, (SMT), 2014.
    [ pdf | bibtex | online ]
  • Integrating SMT solvers in Rodin
    David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. Science of Computer Programming, 2014. DOI: 10.1016/j.scico.2014.04.012.
    [ pdf | bibtex ]

2013

  • Computing prime implicants
    David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013).
    [ pdf | bibtex ]
  • SyMT: finding symmetries in SMT formulas
    Carlos Areces, David Déharbe, Pascal Fontaine, Ezequiel Orbe. (Extended Abstract: Work in progress). 11th International Workshop on Satisfiability Modulo Theories (SMT), 2013.
    [ pdf | bibtex ]
  • Integration of SMT-solvers in B and Event-B development environments
    David Déharbe. Science of Computer Programming. Vol. 78, nº 3. p. 310-316. Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau and Steve Reeves. DOI: 10.1016/j.scico.2011.03.007.
    [ pdf | bibtex ]
  • Le solveur SMT veriT
    David Déharbe, Pablo Federico Dobal, Pascal Fontaine. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). Tool demonstration, 2013.
    [ pdf | bibtex ]

2012

  • Combining decision procedures by (model-) equality propagation
    Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Science of Computer Programming, Vol. 77, p. 518-532, 2012. DOI: 10.1016/j.scico.2010.04.003.
    [ pdf | bibtex ]
  • SMT solvers for Rodin
    David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, editors, In Proc. ABZ, volume 7316 of LNCS, pages 194-207, Springer, 2012.
    [ pdf | bibtex ]

2011

  • Quantifier Inference Rules for SMT proofs
    David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo. Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
    [ pdf | bibtex ]
  • Exploiting symmetry in SMT problems
    David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors. In Proc. Conference on Automated Deduction (CADE), volume 6803 of LNCS. pages 222--236, Springer-Verlag, 2011.
    [ pdf | bibtex ] [ pdf (long version) | bibtex ]

2010

  • Exploring and Exploiting Algebraic and Graphical Properties of Resolution
    Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. In Aarti Gupta and Daniel Kroening editors In Proc. Workshop on Satisfiability Modulo Theories (SMT), 2010.
    [ pdf | bibtex ]
  • GridTPT: a distributed platform for Theorem Prover Testing
    Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. In Boris Konev, Renate Schmidt and Stephan Schulz, editors. In Proc. Workshop on Practical Aspects of Automated Reasoning 2010.
    [ pdf | bibtex ]
  • Integrating SMT-Solvers in Z and B Tools
    Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Oliveira, David Déharbe. Abstract State Machines, Alloy, B and Z (ABZ 2010). Lecture Notes in Computer Science, Vol 5977/2010, p. 412-413, 2010. DOI: 10.1007/978-3-642-11811-1_45.
    [ bibtex ]

2009

  • veriT: an open, trustable and efficient SMT-solver.
    Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. In Renate A. Schmidt, editor. In Proc. Conference on Automated Deduction (CADE), volume 5663 of LNCS, pages 151--156. Springer-Verlag, 2009.
    [ pdf | bibtex ]
  • Combining decision procedures by (model-)equality propagation
    Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. In P. Machado, A. Andrade and A. Duran, editors, In Proc. of the Brazilian Symposium on Formal Methods (SBMF), Salvador, Bahia, Brazil, 2008. volume 240 of Electr. Notes Theor. Comput. Sci., pages 113-128, 2009.
    [ pdf | bibtex ]

Our tools

Several tools are used to support the development of veriT. This section collects our tools that are sufficiently stable for distribution, as well as tools developed by the SMT community and updated for our needs.

Delta SMT

DeltaSMT is a debugging tool developed by Robert Brummayer and Armin Biere at the Institute for Formal Models and Verification at Linz University.

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.

GridTPT

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

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:

  • analyses of SMT-LIB problems (unused variables, typechecking, logic detection)
  • simplifications and transformations of SMT-LIB problems (term normalization, constant propagation) as pre- or post-processing steps.

SMTpp has grown out of veriT and is available under the ISC license. Check out our GitHub page for more detailed information.

SAT solver within Matlab and Octave

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:

  • package for Windows 7 64 bits with Matlab
  • package for Windows 7 32 bits with Matlab
  • package for Linux 64 bits with Matlab
  • package for Linux 64 bits with Octave

External software

veriT relies on third-party software using them either as libraries or as stand-alone applications. veriT is also used or integrated with other software.

GNU MP (is used by veriT)

The GNU Multiple Precision Arithmetic Library is used to represent and manipulate numerical value. It is distributed under the GNU LGPL.

Rodin (integrates veriT)

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 (can be used by veriT)

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.

E (was used by veriT)

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 (was used by veriT)

CRefine is an editor that supports the formal development of concurrent object-oriented software in Circus by implementing a refinement calculus.

Bliss (was used by veriT)

Bliss is a backtracking algorithm for computing automorphism groups and canonical forms of graphs, based on individualization and refinement.

Saucy (was used by veriT)

Saucy is the implementation of a symmetry-discovery algorithm.

PermLib (was used by veriT)

PermLib is a C++ library for permutation computations.

MiniSat (was used by veriT)

In early releases, veriT used the SAT-solver MiniSat to represent and manipulate the boolean structure of the formulas.

Our Team

veriT is current under development by its creators David Déharbe and Pascal Fontaine and other researchers.

David Deharbe's photo

David Déharbe

Lead developer
Associate professor at UFRN/Brazil (team ForAll).

Pascal Fontaine's photo

Pascal Fontaine

Lead developer
Associate professor at University of Lorraine/France (team VeriDis).

Haniel Barbosa's photo

Haniel Barbosa

Developer
PhD student at University of Lorraine/France (team VeriDis).

Past developers have helped a lot:

  • Pablo Federico Dobal developed the SMTpp tool and contributed to the testing infrastructure and the arithmetic reasoning module.
  • Richard Bonichon and Cláudia Tavares developed the SMTpp tool.
  • Diego Caminha Barbosa de Oliveira developed the arithmetic reasoning module and contributed to the combination framework in the theory reasoning engine.
  • Thomas Bouton contributed to the QA infrastructure and the integration of the SAT solver with the theory reasoning engine.

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.

Contact Us

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:

  • Tell us the version of veriT you are using (including the operating system)
  • Try to send us a minimal example that causes the problem

Thanks for helping us improving veriT.