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
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
