cid f281e56c696c0a9fe7f3496e5a7986f29ad65dfd2c46e598109389a8a071f1ee · original · open access · via wikipedia
Title: Cooperating Validity Checker Authors: Venue: Wikipedia Year: unknown Canonical: wiki:cooperating-validity-checker URL: https://en.wikipedia.org/wiki/Cooperating_Validity_Checker Collector: wikipedia OA: true ABSTRACT 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 ; earlier versions include CVC, CVC Lite, and CVC3. 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. cvc5 has bindings for C++, Python, and Java.