Book chapter
CVC: A Cooperating Validity Checker
Computer Aided Verification, pp.500-504
Lecture Notes in Computer Science, Springer Berlin Heidelberg
09/20/2002
DOI: 10.1007/3-540-45657-0_40
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.
Details
- Title: Subtitle
- CVC: A Cooperating Validity Checker
- Creators
- Aaron Stump - Stanford UniversityClark W. Barrett - Stanford UniversityDavid L. Dill - Stanford University
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.500-504
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/3-540-45657-0_40
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 09/20/2002
- Academic Unit
- Computer Science
- Record Identifier
- 9984259462602771
Metrics
1 Record Views