CVC: A cooperating validity checker

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

Research output: Contribution to journalArticle

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)
Pages (from-to)500-504
Number of pages5
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2404
StatePublished - Jan 1 2002

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this