<div>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:</div><div><br></div><div><a href="http://cvc4.cs.nyu.edu" target="_blank">http://cvc4.cs.nyu.edu</a></div>




<div><br></div><div>CVC4 is the latest in the CVC series of SMT solvers and provides the functionality of its predecessors while dramatically boosting performance.  Features include:</div><div><br></div><div> - support for the native (CVC) language as well as the SMT-LIB standard language</div>




<div> - decision procedures for the following theories and their combination:</div><div>      equality with uninterpreted functions, real and integer linear arithmetic,</div><div>      bit-vectors, arrays, tuples, records, and user-defined inductive data types;</div>




<div> - support for quantifiers through heuristic instantiation;</div><div> - an interactive text-based interface;</div><div> - a rich API for embedding in other systems (available for C++ and Java);</div><div> - model generation abilities;</div>




<div> - source compatibility with much of the CVC3 API via a "compatibility library";</div><div> - essentially no limit on the use of source or binaries for research or commercial purposes</div><div>      (details on the license can be found on the web site).</div>



<div><br></div><div>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:</div>




<div><br></div><div>  Clark Barrett (NYU, project leader)</div><div>  Cesare Tinelli (U Iowa, project leader)</div><div>  Kshitij Bansal (NYU)</div><div>  François Bobot (Paris-Diderot University)</div><div>  Chris Conway (Google)</div>




<div>  Morgan Deters (NYU)</div><div>  Liana Haderean (NYU)</div><div>  Dejan Jovanović (NYU)</div><div>  Tim King (NYU)</div><div>  Andrew Reynolds (U Iowa)</div><div><br></div><div>The development of CVC4 is supported in part by the following organizations:</div>




<div><br></div><div> - The Air Force Office of Scientific Research (award FA9550-09-1-0596)</div><div> - Intel Corporation</div><div> - The National Science Foundation (grants  0644299,  0914956, 1049495, 1228765, 1228768)</div>


<div>

 - The Semiconductor Research Corporation (contract 2008-TJ-1850)</div><div><br></div><div>Downloads, documentation, tutorials, and more information are available at the CVC4 web site:</div><div><br></div><div><a href="http://cvc4.cs.nyu.edu" target="_blank">http://cvc4.cs.nyu.edu</a></div>




<div><br></div><div>-The CVC4 team</div><div><br></div>