Book chapter
cvc5: A Versatile and Industrial-Strength SMT Solver
Springer International Publishing
01/01/2022
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.
Details
- Title: Subtitle
- cvc5: A Versatile and Industrial-Strength SMT Solver
- Creators
- Haniel Barbosa - Universidade Federal de Minas GeraisClark Barrett - Stanford UniversityMartin Brain - City, University of LondonGereon Kremer - Stanford UniversityHanna Lachnitt - Stanford UniversityMakai Mann - Stanford UniversityAbdalrhman Mohamed - University of IowaMudathir Mohamed - University of IowaAina Niemetz - Stanford UniversityAndres Nötzli - Stanford UniversityAlex Ozdemir - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - University of IowaYing Sheng - Stanford UniversityCesare Tinelli - University of IowaYoni Zohar - Stanford University
- Resource Type
- Book chapter
- DOI
- 10.1007/978-3-030-99524-9_24
- Publisher
- Springer International Publishing
- Language
- English
- Date published
- 01/01/2022
- Academic Unit
- Computer Science
- Record Identifier
- 9984259429902771
Metrics
93 Record Views