CVC Lite: A New Implementation of the Cooperating Validity Checker Category B

By Clark W. Barrett, S. Berezin. International Conference on Computer Aided Verification, 2004

329 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/646969e807c9c9bc86e2c45f5e836e2ff8acc417

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

CUTE: a concolic unit testing engine for C (2005, methodology): “The solver first builds an equivalence graph based on (dis)equalities (similar to checking satisfiability in theory of equality [2]) and then based on this graph, assigns values to pointers.”
Splitting on Demand in SAT Modulo Theories (2006, methodology): “Some of the ideas formalized in this paper on centralizing case splits in the Boolean engine are implemented in the system SVC [BDL96] and and its successors CVC [BDS02]. and CVC-Lite [BB04].”
All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) (2010, methodology): “For example, many application domains pass the generated formulas to a SMT solver [4, 32].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “Among these, the family of cooperating validity checker (CVC) tools [21,26, 27,132] have played an important role, both in research and in practice [11,48, 70,137,138].”
A Decision Procedure for Bit-Vectors and Arrays (2007, methodology): “STP’s architecture is different from most decision procedures that support both bit-vectors and arrays [18,2,9], which are based on backtracking and a framework for combining specialized theories such as Nelson-Oppen [15].”
Efficient E-Matching for SMT Solvers (2007, unknown): “E-matching is also used in the several other state-of-the-art SMT solvers: CVC3 [3], Fx7 [4], Verifun [5], Yices [6], Zap [7].”
A Fast Linear-Arithmetic Solver for DPLL(T) (2006, methodology): “For general linear arithmetic, existing tools rely either on FourierMotzkin elimination [3] (used by CVClite [4], CVC [5], SVC [6]) or on Simplex methods [7] (used by MathSat [8], ICS [9], Simplics, Yices, ARIO [10]).”
Merge: a programming model for heterogeneous multi-core systems (2008, methodology): “At compile time the predicates are converted to logical axioms that can be used with an automated theorem prover CVC3 ( 3 ) to determine specificity and exhaustiveness (similar to the methodology and implementation in JPred (22)).”
Handbook of Satisfiability (2021, methodology): “In this form, splitting on demand is implemented in the CVC, CVC Lite and CVC3 systems [144, 13, 18].”
What's Decidable About Arrays? (2006, methodology): “We used CVC Lite [2] as the underlying decision procedure.”