Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution


CVC4 is the latest version of the Cooperating Validity Checker. A joint project of NYU and U Iowa, CVC4 aims to support the useful feature set of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances. CVC4 represents a completely new code base; it is a from-scratch rewrite of CVC3, and many subsystems have been completely redesigned. Additional decision procedures for CVC4 are currently under development, but for what it currently achieves, it is a lighter-weight and higher-performing tool than CVC3. We describe the system architecture, subsystems of note, and discuss some applications and continuing work.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Number of pages7
StatePublished - 2011
Event23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT, United States
Duration: Jul 14 2011Jul 20 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6806 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other23rd International Conference on Computer Aided Verification, CAV 2011
Country/TerritoryUnited States
CitySnowbird, UT

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'CVC4'. Together they form a unique fingerprint.

Cite this