CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


CI

3 December 2012

Announcing the Release of CVC4, Version 1.0

by Dejan Jovanović

This news post contains outdated information (e.g. links, instructions). Please refer to newer documentation for up-to-date information.

We are pleased to announce the first public release of CVC4, version 1.0, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.

CVC4 is the latest in the CVC series of SMT solvers and provides the functionality of its predecessors while dramatically boosting performance. Features include:

We welcome feedback, feature requests, contributions, and collaborations. It is our hope that CVC4 will become a research platform for a broad and diverse set of users and developers. If you are interested in getting involved with the project, please contact a member of the development team:

The development of CVC4 is supported in part by the following organizations:

Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.nyu.edu.

– The CVC4 team