CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
CVC4 is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. A joint project of NYU and U Iowa, CVC4 aims to support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances.
CVC4 is intended to be an open and extensible SMT engine, and it can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license). Contributors to CVC4 are required to sign a Contributor License Agreement (CLA), which can be found here.
The fifth stable release of CVC4 (version 1.4) has been officially released. It is available for download (as are nightly development builds).
CVC4 works with a version of first-order logic with polymorphic types and has a wide variety of features including:
- several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit-vectors, strings, and equality over uninterpreted function symbols;
- support for quantifiers;
- an interactive text-based interface;
- a rich C++ API for embedding in other systems;
- model generation abilities.
Go to our new download page here.
Please send all bug reports to email@example.com, or use the CVC4 issue tracker. If you have a question, a feature request, or would like to contribute in some way, please contact one of the project leaders. The CVC-USERS list is for users of CVC3 and CVC4. We will make periodic announcements to this list and users are also encouraged to use it for discussion.
If you are a CVC4 user with an interesting application, and you would like to share your experience with other CVC4 users, we encourage you to write a description in our designated open wiki page.
History of CVC
The Cooperating Validity Checker series has a long history. The Stanford Validity Checker (SVC) came first in 1996, incorporating theories and its own SAT solver. Its successor, the Cooperating Validity Checker (CVC), had a more optimized internal design, produced proofs, used the Chaff SAT solver, and featured a number of usability enhancements. Its name comes from the cooperative nature of decision procedures in Nelson-Oppen theory combination, which share amongst each other equalities between shared terms. CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to make CVC more flexible (hence the “lite”) while extending the feature set: CVC Lite supported quantifiers where its predecessors did not. CVC3 was a major overhaul of portions of CVC Lite: it added better decision procedure implementations, added support for using MiniSat in the core, and had generally better performance.
CVC4 is the new version, the fifth generation of this validity checker line that is now celebrating sixteen years of heritage. It represents a complete re-evaluation of the core architecture to be both performant and to serve as a cutting-edge research vehicle for the next several years. Rather than taking CVC3 and redesigning problem parts, we’ve taken a clean-room approach, starting from scratch. Before using any designs from CVC3, we have thoroughly scrutinized, vetted, and updated them. Many parts of CVC4 bear only a superficial resemblance, if any, to their correspondent in CVC3.
However, CVC4 is fundamentally similar to CVC3 and many other modern SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and a delegation path to different decision procedure implementations, each in charge of solving formulas in some background theory.
The re-evaluation and ground-up rewrite was necessitated, we felt, by the performance characteristics of CVC3. CVC3 has many useful features, but some core aspects of the design led to high memory use, and the use of heavyweight computation (where more nimble engineering approaches could suffice) makes CVC3 a much slower prover than other tools. As these designs are central to CVC3, a new version was preferable to a selective re-engineering, which would have ballooned in short order.
- Kshitij Bansal, New York University, Google
- Clark Barrett, New York University, Google, Stanford University
- Francois Bobot, The University of Iowa, Commissariat a l’Energie Atomique
- Martin Brain, University of Oxford
- Christopher Conway, New York University, Google
- Morgan Deters, New York University (in memoriam)
- Liana Hadarean, New York University, Mentor Graphics Corporation
- Dejan Jovanovic, New York University, SRI International
- Guy Katz, New York University, Stanford University
- Tim King, New York University, Universite Joseph Fourier, Google
- Tianyi Liang, The University of Iowa
- Paul Meng, The University of Iowa
- Andres Noetzli, Stanford University
- Andrew Reynolds, The University of Iowa, EPFL
- Cesare Tinelli, The University of Iowa
CVC4 is supported in part by the following organizations:
- The Air Force Office of Scientific Research (award FA9550-09-1-0596)
- The Defense Advanced Research Projects Agency (awards FA8750-13-2-0241, FA8750-I5-C-0113)
- The European Research Council (grant 306595 “STATOR”)
- GE Global Research
- Intel Corporation
- The National Science Foundation (grants 0644299, 0914956, 1049495, 1228768, 1320583)
- The Semiconductor Research Corporation (tasks 1850.001, 1850.002)
Any opinions, findings and conclusions or recommendations expressed in this site are those of the authors and do not necessarily reflect the views of the organizations listed above.