An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Try cvc5 online!

View on GitHub
Join the Conversation
Third Party Applications

GitHub LinkedIn Twitter Facebook

License: BSD


If you are citing cvc5, please use the following BibTex entry :

  author    = {Haniel Barbosa and
               Clark W. Barrett and
               Martin Brain and
               Gereon Kremer and
               Hanna Lachnitt and
               Makai Mann and
               Abdalrhman Mohamed and
               Mudathir Mohamed and
               Aina Niemetz and
               Andres N{\"{o}}tzli and
               Alex Ozdemir and
               Mathias Preiner and
               Andrew Reynolds and
               Ying Sheng and
               Cesare Tinelli and
               Yoni Zohar},
  editor    = {Dana Fisman and
               Grigore Rosu},
  title     = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 28th International Conference, {TACAS} 2022, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {13243},
  pages     = {415--442},
  publisher = {Springer},
  year      = {2022},
  url       = {https://doi.org/10.1007/978-3-030-99524-9\_24},
  doi       = {10.1007/978-3-030-99524-9\_24},
  timestamp = {Fri, 01 Apr 2022 15:49:27 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},


Conference Papers

Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. Cvc5: A Versatile And Industrial-strength Smt Solver . In Tools and algorithms for the construction and analysis of systems - 28th international conference, TACAS 2022, held as part of the european joint conferences on theory and practice of software, ETAPS 2022, munich, germany, april 2-7, 2022, proceedings, part I, vol. 13243, Lecture notes in computer science, pp. 415-442, Springer. (2022)
SCP Best Tool Paper Award
PDF DOI Slides Bibtex Artifact

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett and Cesare Tinelli. Bit-precise Reasoning Via Int-blasting . In Verification, model checking, and abstract interpretation - 23rd international conference, VMCAI 2022, philadelphia, PA, USA, january 16-18, 2022, proceedings, vol. 13182, Lecture notes in computer science, pp. 496-518, Springer. (2022)
PDF DOI Slides Bibtex Artifact