18 lines
902 B
Markdown
18 lines
902 B
Markdown
# cvc4
|
|
|
|
[CVC4](https://cvc4.github.io/) 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.
|