“cvc5: A Versatile and Industrial-Strength SMT Solver” by 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. In Proceedings of the 28^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), (Dana Fisman and Grigore Rosu, eds.), Apr. 2022, pp. 415-442. \em Best SCP Tool Paper Award.
cvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5's architectural design and highlights the major features and components introduced since CVC4 1.8. We evaluate cvc5's performance on all benchmarks in SMT-LIB and provide a comparison against CVC4 and Z3.
BibTeX entry:
@inproceedings{BBB+22,
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 = {Proceedings of the {\it 28^{th}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '22)},
series = {Lecture Notes in Computer Science},
volume = {13243},
pages = {415--442},
publisher = {Springer},
month = apr,
year = {2022},
doi = {10.1007/978-3-030-99524-9_24},
note = {\em Best SCP Tool Paper Award.},
url = {http://theory.stanford.edu/~barrett/pubs/BBB+22.pdf}
}
(This webpage was created with bibtex2web.)