CVC

A cooperating validity checker

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

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

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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 14th International Conference, CAV 2002, Proceedings
PublisherSpringer Verlag
Pages500-504
Number of pages5
Volume2404
ISBN (Print)9783540439974
StatePublished - 2002
Event14th International Conference on Computer Aided Verification, CAV 2002 - Copenhagen, Denmark
Duration: Jul 27 2002Jul 31 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2404
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th International Conference on Computer Aided Verification, CAV 2002
CountryDenmark
CityCopenhagen
Period7/27/027/31/02

Fingerprint

Decision Procedures
Union
High Performance
Reasoning
Valid
Logic

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Stump, A., Barrett, C. W., & Dill, D. L. (2002). CVC: A cooperating validity checker. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings (Vol. 2404, pp. 500-504). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404). Springer Verlag.

CVC : A cooperating validity checker. / Stump, Aaron; Barrett, Clark W.; Dill, David L.

Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. p. 500-504 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404).

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

Stump, A, Barrett, CW & Dill, DL 2002, CVC: A cooperating validity checker. in Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. vol. 2404, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2404, Springer Verlag, pp. 500-504, 14th International Conference on Computer Aided Verification, CAV 2002, Copenhagen, Denmark, 7/27/02.
Stump A, Barrett CW, Dill DL. CVC: A cooperating validity checker. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404. Springer Verlag. 2002. p. 500-504. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Stump, Aaron ; Barrett, Clark W. ; Dill, David L. / CVC : A cooperating validity checker. Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. pp. 500-504 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{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’ 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",
language = "English (US)",
isbn = "9783540439974",
volume = "2404",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "500--504",
booktitle = "Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings",

}

TY - GEN

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

M3 - Conference contribution

SN - 9783540439974

VL - 2404

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

SP - 500

EP - 504

BT - Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings

PB - Springer Verlag

ER -