CVC4

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

doi:10.1007/978-3-642-22110-1_14

CVC4

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Pages	171-177
Number of pages	7
DOIs	https://doi.org/10.1007/978-3-642-22110-1_14
State	Published - 2011
Event	23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT, United States Duration: Jul 14 2011 → Jul 20 2011

Publication series

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

Other

Other	23rd International Conference on Computer Aided Verification, CAV 2011
Country/Territory	United States
City	Snowbird, UT
Period	7/14/11 → 7/20/11

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

Cite this

Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., & Tinelli, C. (2011). CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings (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 et al.
Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. 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 proceeding › Conference 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. 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

@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{\'c} 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",

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

AN - SCOPUS:79960377581

SN - 9783642221095

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

T2 - 23rd International Conference on Computer Aided Verification, CAV 2011

Y2 - 14 July 2011 through 20 July 2011

ER -

CVC4

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this