computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

and

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

, 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. Both CVC4 and cvc5 support the

SMT-LIB In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involv ...

and TPTP input formats for solving SMT problems, and the SyGuS-IF format for

program synthesis In computer science, program synthesis is the task to construct a computer program, program that provably correct, provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rat ...

. 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 Java is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea (a part of Pacific Ocean) to the north. With a population of 156.9 million people (including Madura) in mid 2024, proje ...

. CVC4 competed in SMT-COMP in the years 2014-2020, and cvc5 has competed in the years 2021-2022. CVC4 competed in SyGuS-COMP in the years 2015-2019, and in CASC in 2013-2015. CVC4 uses the DPLL(T) architecture, and supports the theories of linear arithmetic over rationals and

integer An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...

s, fixed-width bitvectors,

floating-point arithmetic In computing, floating-point arithmetic (FP) is arithmetic on subsets of real numbers formed by a ''significand'' (a Sign (mathematics), signed sequence of a fixed number of digits in some Radix, base) multiplied by an integer power of that ba ...

string String or strings may refer to: *String (structure), a long flexible structure made from threads twisted together, which is used to tie, bind, or hang other objects Arts, entertainment, and media Films * ''Strings'' (1991 film), a Canadian anim ...

s, (co)-datatypes,

sequence In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is cal ...

s (used to model

dynamic array In computer science, a dynamic array, growable array, resizable array, dynamic table, mutable array, or array list is a random access, variable-size list data structure that allows elements to be added or removed. It is supplied with standard l ...

s), finite sets and relations,

separation logic In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertio ...

, and uninterpreted functions among others. cvc5 additionally supports

finite field In mathematics, a finite field or Galois field (so-named in honor of Évariste Galois) is a field (mathematics), field that contains a finite number of Element (mathematics), elements. As with any field, a finite field is a Set (mathematics), s ...

s. In addition to standard SMT and SyGuS solving, cvc5 supports

abductive reasoning Abductive reasoning (also called abduction,For example: abductive inference, or retroduction) is a form of logical inference that seeks the simplest and most likely conclusion from a set of observations. It was formulated and advanced by Ameri ...

, which is the problem of constructing a formula that can be conjoined with a formula to prove a goal formula . cvc5 has been subject to several independent test campaigns.

Applications

CVC4 has been applied to the synthesis of recursive programs. and to the verification of

Amazon Web Services Amazon Web Services, Inc. (AWS) is a subsidiary of Amazon.com, Amazon that provides Software as a service, on-demand cloud computing computing platform, platforms and Application programming interface, APIs to individuals, companies, and gover ...

access policies. CVC4 and cvc5 have been integrated with Coq and Isabelle. CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.

References

* * {{Cite book , last1=Barrett , first1=Clark , last2=Conway , first2=Christopher L. , last3=Deters , first3=Morgan , last4=Hadarean , first4=Liana , last5=Jovanović , first5=Dejan , last6=King , first6=Tim , last7=Reynolds , first7=Andrew , last8=Tinelli , first8=Cesare , chapter=CVC4 , date=2011 , editor-last=Gopalakrishnan , editor-first=Ganesh , editor2-last=Qadeer , editor2-first=Shaz , title=Computer Aided Verification , chapter-url=https://link.springer.com/chapter/10.1007/978-3-642-22110-1_14 , series=Lecture Notes in Computer Science , volume=6806 , language=en , location=Berlin, Heidelberg , publisher=Springer , pages=171–177 , doi=10.1007/978-3-642-22110-1_14 , isbn=978-3-642-22110-1 Free and open-source software Free software programmed in C++ Satisfiability modulo theories solvers Software using the BSD license