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.
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.
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]
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]
^Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo Theories", Handbook of Model Checking, Cham: Springer International Publishing, pp. 305–343,
doi:10.1007/978-3-319-10575-8_11,
ISBN978-3-319-10575-8
^Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022).
"Flexible Proof Production in an Industrial-Strength SMT Solver". In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning. Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35.
doi:
10.1007/978-3-031-10769-6_3.
ISBN978-3-031-10769-6.
S2CID250164402.
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.
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.
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]
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]
^Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo Theories", Handbook of Model Checking, Cham: Springer International Publishing, pp. 305–343,
doi:10.1007/978-3-319-10575-8_11,
ISBN978-3-319-10575-8
^Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022).
"Flexible Proof Production in an Industrial-Strength SMT Solver". In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning. Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35.
doi:
10.1007/978-3-031-10769-6_3.
ISBN978-3-031-10769-6.
S2CID250164402.