cvc5: A Versatile and Industrial-Strength SMT Solver
Barbosa, H., Barrett, C., Brain, M. 
ORCID: 0000-0003-4216-7151 , Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C. & Zohar, Y. (2022).
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, 2–7 Apr 2022, Munich, Germany.
doi: 10.1007/978-3-030-99524-9_24
Abstract
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.
| Publication Type: | Conference or Workshop Item (Paper) |
|---|---|
| Publisher Keywords: | automated reasoning, constraint solving, satisfiability modulo theories, cvc5, Artificial Intelligence & Image Processing, 46 Information and computing sciences |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Departments: | School of Science & Technology School of Science & Technology > Department of Computer Science |
| Related URLs: | |
| SWORD Depositor: |
Available under License Creative Commons Attribution.
Download (925kB) | Preview
Export
Downloads
Downloads per month over past year
Metadata
MetadataActions (login required)
Admin Login