Cooperating Validity Checker
SMT solver From Wikipedia, the free encyclopedia
In computer science and mathematical logic, 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); earlier versions include CVC, CVC Lite, and CVC3.[2] Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats.[3][4] cvc5 has bindings for C++, Python, and Java.
 | This article may be too technical for most readers to understand. (November 2023) |
| Developer(s) | Stanford University and University of Iowa |
|---|---|
| Initial release | 2022 |
| Stable release | 1.2.1[1]
/ January 28, 2025 |
| Written in | C++ |
| Operating system | Windows, Linux, macOS |
| Type | Theorem prover |
| License | BSD 3-clause |
| Website | cvc5 |
CVC4 competed in SMT-COMP in the years 2014-2020,[5] and cvc5 has competed in the years 2021-2022.[6] CVC4 competed in SyGuS-COMP in the years 2015-2019,[7] and in CASC in 2013-2015.
CVC4 uses the DPLL(T) architecture,[8] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,[9] floating-point arithmetic,[10] strings,[11] (co)-datatypes,[12] sequences (used to model dynamic arrays),[13] finite sets and relations,[14][15] separation logic,[16] and uninterpreted functions among others. cvc5 additionally supports finite fields.[17]
In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning, which is the problem of constructing a formula B that can be conjoined with a formula A to prove a goal formula C.[18][19]
cvc5 has been subject to several independent test campaigns.[20]
Applications
CVC4 has been applied to the synthesis of recursive programs.[21] and to the verification of Amazon Web Services access policies.[22][23] CVC4 and cvc5 have been integrated with Coq[24] and Isabelle.[25] CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.[26]
References
Wikiwand - on
Seamless Wikipedia browsing. On steroids.