[FOM] Announcing the release of CVC4, version 1.0

[Clark Barrett]

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>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>http://cvc4.cs.nyu.edu

-The CVC4 team

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20121203/ca2803eb/attachment.html>