An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
View on GitHub
Downloads
Documentation
Tutorials
Blog
Join the Conversation
People
Publications
Awards
Third Party Applications
Acknowledgements
Newsletter
If you are citing cvc5, please use the following BibTex entry :
@inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22, 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}, }
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