CVC: A cooperating validity checker

Aaron Stump; Clark W. Barrett; David L. Dill

doi:10.1007/3-540-45657-0_40

CVC: A cooperating validity checker

Aaron Stump, Clark W. Barrett, David L. Dill

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories’ union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.

Original language	English (US)
Pages (from-to)	500-504
Number of pages	5
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2404
DOIs	https://doi.org/10.1007/3-540-45657-0_40
State	Published - 2002

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-45657-0_40

Cite this

@article{1380ff4d9e44406289baf7b3157f5032,

title = "CVC: A cooperating validity checker",

abstract = "Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories{\textquoteright} union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.",

author = "Aaron Stump and Barrett, {Clark W.} and Dill, {David L.}",

year = "2002",

doi = "10.1007/3-540-45657-0_40",

language = "English (US)",

volume = "2404",

pages = "500--504",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - CVC

T2 - A cooperating validity checker

AU - Stump, Aaron

AU - Barrett, Clark W.

AU - Dill, David L.

PY - 2002

Y1 - 2002

N2 - Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories’ union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.

AB - Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories’ union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.

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

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

U2 - 10.1007/3-540-45657-0_40

DO - 10.1007/3-540-45657-0_40

M3 - Article

AN - SCOPUS:84937554711

SN - 0302-9743

VL - 2404

SP - 500

EP - 504

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

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

ER -

CVC: A cooperating validity checker

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this