Cooperating Validity Checker
| Developer(s) | Stanford University and University of Iowa |
|---|---|
| Initial release | 2022 |
| Stable release | 1.0.8[1]
/ 31 August 2023 |
| Written in | C++ |
| Operating system | Windows, Linux, macOS |
| Type | Theorem prover |
| License | BSD 3-clause |
| Website | cvc5 |
Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 (stylized cvc5). Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. cvc5 has bindings for C++, Python, and Java.
CVC4 competed in SMT-COMP in the years 2014-2020,[2] and cvc5 has competed in the years 2021-2022.[3] CVC4 competed in SyGuS-COMP in the years 2015-2019,[4] and in CASC in 2013-2015.
CVC4 uses the DPLL(T) architecture,[5] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,[6], strings,[7], (co)-datatypes,[8], sequences, finite sets and relations, and separation logic, among others.
Applications
![[icon]](/wiki/File:Wiki_letter_w_cropped.svg?lang=en){kind=small} | This section needs expansion. You can help by adding to it. (November 2023) |
CVC4 has been applied to the synthesis of recursive programs.[9] and to the verification of Amazon Web Services access policies.[10]
References
- ^ "Release cvc5-1.0.8 · cvc5/cvc5". GitHub. Retrieved 2023-11-29.
- ^ "Participants". SMT-COMP. Retrieved 2023-11-29.
- ^ "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.
- ^
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and Analysis of SyGuS-Comp'15". Electronic Proceedings in Theoretical Computer Science. 202: 3–26. doi:10.4204/EPTCS.202.3. ISSN 2075-2180.
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 229: 178–202. doi:10.4204/EPTCS.229.13. ISSN 2075-2180.
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 260: 97–115. doi:10.4204/EPTCS.260.9. ISSN 2075-2180.
- ^ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). Biere, Armin; Bloem, Roderick (eds.). "A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9.
- ^ Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). Biere, Armin; Bloem, Roderick (eds.). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
- ^ Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). Lutz, Carsten; Ranise, Silvio (eds.). "A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings". Frontiers of Combining Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
- ^ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). Felty, Amy P.; Middeldorp, Aart (eds.). "A Decision Procedure for (Co)datatypes in SMT Solvers". Automated Deduction - CADE-25. Lecture Notes in Computer Science. Cham: Springer International Publishing: 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
- ^ Berman, Shmuel (2021-10-17). "Programming-by-example by programming-by-example: synthesis of looping programs". Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity. SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery: 19–21. doi:10.1145/3484271.3484977. ISBN 978-1-4503-9088-0.
- ^ Rungta, Neha (2022). Shoham, Sharon; Vizel, Yakir (eds.). "A Billion SMT Queries a Day (Invited Paper)". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 3–18. doi:10.1007/978-3-031-13185-1_1. ISBN 978-3-031-13185-1.
{{cite journal}}: no-break space character in|title=at position 24 (help)
- Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). Fisman, Dana; Rosu, Grigore (eds.). "cvc5: A Versatile and Industrial-Strength SMT Solver". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 415–442. doi:10.1007/978-3-030-99524-9_24. ISBN 978-3-030-99524-9.
- Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). "CVC4". Computer Aided Verification. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 171–177. doi:10.1007/978-3-642-22110-1_14. ISBN 978-3-642-22110-1.