CVC lite: A new implementation of the cooperating validity checker. Category B

Clark Barrett, Sergey Berezin

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

We describe a tool called CVC Lite (CVCL), an automated theorem prover for formulas in a union of first-order theories. CVCL supports a set of theories which are useful in verification, including uninterpreted functions, arrays, records and tuples, and linear arithmetic. New features in CVCL (beyond those provided in similar previous systems) include a library API, more support for producing proofs, some heuristics for reasoning about quantifiers, and support for symbolic simulation primitives.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRajeev Alur, Doron A. Peled
PublisherSpringer Verlag
Pages515-518
Number of pages4
ISBN (Print)3540223428, 9783540223429
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3114
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'CVC lite: A new implementation of the cooperating validity checker. Category B'. Together they form a unique fingerprint.

  • Cite this

    Barrett, C., & Berezin, S. (2004). CVC lite: A new implementation of the cooperating validity checker. Category B. In R. Alur, & D. A. Peled (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 515-518). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3114). Springer Verlag. https://doi.org/10.1007/978-3-540-27813-9_49