CVC Lite Documentation

Quick References:

• CVC Lite Home Page
• README
• LICENSE
• INSTALL
• The CVC Lite User Manual
• HOWTO Write a Decision Procedure in CVC Lite
• Savannah Interface (for bug reports, support requests, developers' tasks, etc.)

---

Welcome to the world of CVC Lite documentation! Here you will find plenty of information about the code and programming interfaces of CVC Lite (perhaps, more than you ever need to know), and some information about the interactive program called cvcl.

CVC Lite is an efficient decision procedure for quantifier-free first-order logic over several interpreted theories (linear arithmetic, uninterpreted functions, arrays, etc.). It is actively developed by the Formal Verification Group at Stanford University and the Analysis of Computer Systems (ACSys) group at New York University.

The theoretical basis of CVC Lite is the framework for cooperating decision procedures developed by Clark Barrett. Roughly speaking, the theoretical framework is a happy marriage of Nelson-Oppen and Shostak methods with some enhancements and bug fixes.

It is a complete rewrite of the Cooperating Validity Checker (CVC), originally written by Aaron Stump. CVC, in turn, was a rewrite of the Stanford Validity Checker (SVC). That is, we are talking about a third-generation tool here, so it had better be good...

There are several ways to use CVC Lite. First, it can be used as an existing decision procedure to solve the validity of various formulas that happen to be lying around. This can be done in two ways:

• CVC Lite can be used as an interactive tool with a fairly advanced input language for humans, and with a fairly simple LISP-like input language for other programs (in the very near future). Refer to The CVC Lite User Manual for more information.

• CVC Lite can be used as a C++ library (there is also a C interface) linked to your own tool. This way is more efficient and is independent of the actual input language. For that, you will need to read the code documentation for the ValidityChecker class, and probably some other related APIs.

Another way is to use the CVC Lite framework is by implementing your own decision procedure and incorporating it into the tool, thereby extending the input language with yet another interpreted theory. If you are interested in becoming a decision procedure developer (or a DP-developer for short), you'll need to read HOWTO Write a Decision Procedure in CVC Lite, and study the Theory API in the code documentation. Reading Clark Barrett's Ph.D. thesis will also help.

Finally, CVC Lite can be used as a complex and challenging programming project for testing your coding abilities, and for providing (under)graduate students with a hands-on experience in software design in formal methods. Let us know if you are interested in helping with the core development of CVC Lite.

---