@inbook{68c6419a1f4c477aa8b097b9f38a4661,
title = "CVC lite: A new implementation of the cooperating validity checker. Category B",
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.",
author = "Clark Barrett and Sergey Berezin",
year = "2004",
doi = "10.1007/978-3-540-27813-9_49",
language = "English (US)",
isbn = "3540223428",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "515--518",
editor = "Rajeev Alur and Peled, {Doron A.}",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}