CVC4

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

Abstract

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
Pages171-177
Number of pages7
Volume6806 LNCS
DOIs
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)03029743
ISSN (Electronic)16113349

Other

Other23rd International Conference on Computer Aided Verification, CAV 2011
CountryUnited States
CitySnowbird, UT
Period7/14/117/20/11

Fingerprint

Surface mount technology
Decision Procedures
System Architecture
Subsystem
Engineering
Design

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., ... Tinelli, C. (2011). CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings (Vol. 6806 LNCS, pp. 171-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS). https://doi.org/10.1007/978-3-642-22110-1_14

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

Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Vol. 6806 LNCS 2011. p. 171-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6806 LNCS).

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

Barrett, C, Conway, CL, Deters, M, Hadarean, L, Jovanović, D, King, T, Reynolds, A & Tinelli, C 2011, CVC4. in Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. vol. 6806 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6806 LNCS, pp. 171-177, 23rd International Conference on Computer Aided Verification, CAV 2011, Snowbird, UT, United States, 7/14/11. https://doi.org/10.1007/978-3-642-22110-1_14
Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T et al. CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Vol. 6806 LNCS. 2011. p. 171-177. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-22110-1_14
Barrett, Clark ; Conway, Christopher L. ; Deters, Morgan ; Hadarean, Liana ; Jovanović, Dejan ; King, Tim ; Reynolds, Andrew ; Tinelli, Cesare. / CVC4. Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. Vol. 6806 LNCS 2011. pp. 171-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f09a994e9efc4bbea489c5fe1fdbf428,
title = "CVC4",
abstract = "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.",
author = "Clark Barrett and Conway, {Christopher L.} and Morgan Deters and Liana Hadarean and Dejan Jovanović and Tim King and Andrew Reynolds and Cesare Tinelli",
year = "2011",
doi = "10.1007/978-3-642-22110-1_14",
language = "English (US)",
isbn = "9783642221095",
volume = "6806 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "171--177",
booktitle = "Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings",

}

TY - GEN

T1 - CVC4

AU - Barrett, Clark

AU - Conway, Christopher L.

AU - Deters, Morgan

AU - Hadarean, Liana

AU - Jovanović, Dejan

AU - King, Tim

AU - Reynolds, Andrew

AU - Tinelli, Cesare

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79960377581&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79960377581&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22110-1_14

DO - 10.1007/978-3-642-22110-1_14

M3 - Conference contribution

SN - 9783642221095

VL - 6806 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 171

EP - 177

BT - Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings

ER -