Announcing the Release of CVC4, Version 1.0

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:

• support for the native (CVC) language as well as the SMT-LIB standard language;
• decision procedures for the following theories and their combination: equality with uninterpreted functions, real and integer linear arithmetic, bit-vectors, arrays, tuples, records, and user-defined inductive data types;
• support for quantifiers through heuristic instantiation;
• an interactive text-based interface;
• a rich API for embedding in other systems (available for C++ and Java);
• model generation abilities;
• source compatibility with much of the CVC3 API via a “compatibility library”;
• essentially no limit on the use of source or binaries for research or commercial purposes (details on the license can be found on the web site).

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:

• Clark Barrett (NYU, project leader)
• Cesare Tinelli (U Iowa, project leader)
• Kshitij Bansal (NYU)
• François Bobot (Paris-Diderot University)
• Chris Conway (Google)
• Morgan Deters (NYU)
• Liana Haderean (NYU)
• Dejan Jovanović (NYU)
• Tim King (NYU)
• Andrew Reynolds (U Iowa)

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

• The Air Force Office of Scientific Research (award FA9550-09-1-0596)
• Intel Corporation
• The National Science Foundation (grants 0644299, 0914956, 1049495, 1228765, 1228768)
• The Semiconductor Research Corporation (contract 2008-TJ-1850)

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

– The CVC4 team