veriT logo
An open, trustable and efficient SMT-solver

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.

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.

Publications

2021

  • Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
    Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. CADE 2021.
    [ pdf ]
  • Alethe: Towards a Generic SMT Proof Format (extended abstract)
    Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. PxTP 2021.
    [ pdf ]
  • Méthodes pour le raisonnement d'ordre supérieur dans SMT
    Daniel El Ouraoui. Ph.D. thesis. Inria, Université de Lorraine
    [ pdf | bibtex ]

2020

  • Politeness and Combination Methods for Theories with Bridging Functions
    Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. Journal of Automated Reasoning, Volume 64, 2020.
    [ pdf | bibtex ]
  • Scalable Fine-Grained Proofs for Formula Processing
    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Journal of Automated Reasoning, Volume 64, 2020.
    [ pdf | bibtex ]
  • Politeness for the Theory of Algebraic Datatypes
    Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, and Clark W. Barrett. IJCAR 2020.
    [ pdf | bibtex ]

2019

  • Extending SMT Solvers to Higher-order Logic
    Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett. CADE 2019.
    [ pdf | bibtex ]
  • Reconstructing VeriT Proofs in Isabelle/HOL
    Mathias Fleury, and Hans-Jörg Schurr. PxTP 2019.
    [ pdf | slides | bibtex ]
  • Theory Combination: Beyond Equality Sharing
    Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, and Cesare Tinelli. Description Logic, Theory Combination, and All That 2019.
    [ pdf | bibtex ]

2018

  • Revisiting Enumerative Instantiation
    Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Tools and Algorithms for the Construction and Analysis of Systems, 2018.
    [ pdf | bibtex ]

2017

  • NP-completeness of small conflict set generation for congruence closure
    Andreas Fellner, Pascal Fontaine, and Bruno Woltzenlogel Paleo. Formal Methods in System Design, Volume 51, 2017.
    [ pdf | bibtex ]
  • 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 ]
  • Congruence Closure with Free Variables (Work in Progress)
    Haniel Barbosa, Pascal Fontaine. 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 Team

veriT was created by David Déharbe and Pascal Fontaine and is developed in collaboration with other researchers.

Pascal Fontaine's photo

Pascal Fontaine

Founder and Lead Developer
Professor at Université de Liège in Belgium
(Montefiore Institute).

Hans-Jörg Schurr's photo

Hans-Jörg Schurr

Lead Developer
PhD student at Inria Nancy Grand Est and Université de Lorraine in Nancy, France

Haniel Barbosa's photo

Haniel Barbosa

Developer
Assistant professor at Universidade Federal de Minas Gerais (UFMG) in Belo Horizonte, Brazil.

David Deharbe's photo

David Déharbe

Founder
Software Engineer and Formal Methods Expert at Clearsy.

Past developers have helped a lot:

  • Daniel El Ouraoui developed support for higher-order logic within quantifier instantiation and worked on instantiation heuristics including some based on machine learning.
  • 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.

Special thanks to:

  • Jasmin Blanchette funded some of the veriT development within the Matryoshka project and provided countless invaluable advice and suggestions.
  • Mathias Fleury implemented the reconstruction of veriT's proofs in Isabelle/HOl. During this he helped to improve the proof output.
  • Chantal Keller implemented SMTCoq.

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.

Tools

We use several tools to develop veriT or integrate veriT.

SMT-LIB

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: veriT as tactic and Sledgehammer backend

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.

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.

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.

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.