More about CVC

The problem CVC is solving

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

linear real arithmetic (operators are addition, subtraction, less-than, and multiplication and division by a constant)
arrays (operations are reading from an array and updating an array at a given index)
inductive datatypes (e.g., lists and trees; records and tuples are special cases)

CVC combines independent cooperating decision procedures for these theories into a decision procedure for the combination of the theories. CVC is open-ended, in the sense that (under certain restrictions) new independent decision procedures can be added to the system in a provably correct way. CVC achieves this by implementing a version of the Nelson-Oppen framework.

Propositional reasoning

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).

Proof production

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.

Other features

Arbitrary precision arithmetic is supported using the Gnu MP library.

History

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 large examples.

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.