[TYPES/announce] Announcing the release of CVC4, version 1.0

[Dejan Jovanović]

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