CVC decides logical validity of quantifier-free formulas in classical first-order logic with equality, enriched with certain background theories. In the current release, the background theories are for
For propositional reasoning, CVC incorporates Chaff, a
state-of-the-art SAT solver. On large examples with many
propositional connectives, using Chaff can greatly reduce the running
time required to test validity of the formula. Run CVC with the
"+sat" command-line option to turn on Chaff (which is off by default).
CVC can emit independently checkable proofs of valid formulas. The
proofs can be checked by a much simpler proof-checker, called flea,
which is included in the distribution of CVC. See the documentation for details on how to produce
proofs from CVC. Proof production is currently not available when
Chaff is on.
Arbitrary precision arithmetic is supported using the Gnu MP library.
The predecessor to CVC is the Stanford Validity
Checker (SVC). CVC improves on SVC by having a much more solid
theoretical foundation, more robust and extensible implementation,
improved input language, proof production, and new theories. By
incorporating the Chaff SAT solver, CVC is able to outperform SVC on
Authors and Contributors
The main designer of the framework implemented by CVC is Clark Barrett, who also added Chaff to CVC. The CVC project is led by Prof. David L. Dill. Support for arbitrary precision arithmetic was added by Sergey Berezin and Vijay Ganesh. The main implementor of CVC, main designer of the subsidiary decision procedures, and author of these web pages is Aaron Stump.