CVC4 1.3 Released

This news post contains outdated information (e.g. links, instructions). Please refer to newer documentation for up-to-date information.

We are delighted to announce version 1.3 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.

Version 1.3 adds improved SMT-LIB support, a new decision procedure for string constraints, support for TPTP’s TFF and TFA formats, and numerous improvements to the library interface, especially the Java language bindings.

Additionally, this release:

• adds support for new arithmetic operations which were previously missing (abs, to_real, to_int, and is_int)
• adds support for bitvector-integer conversion operations (bv2nat and int2bv)
• includes important bug fixes and performance improvements over the previous stable release (version 1.2)

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 Hadarean (NYU)
• Dejan Jovanović (NYU)
• Tim King (NYU)
• Tianyi Liang (U Iowa)
• 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)
• The Defense Advanced Research Projects Agency (award FA8750-13-2-0241)
• Intel Corporation
• The National Science Foundation (grants 0644299, 0914956, 1049495, 1228765, 1228768, 1320583, 1347900)
• The Semiconductor Research Corporation (tasks 1850.001, 1850.002)

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

-The CVC4 team