CVC: A cooperating validity checker. 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.

References in zbMATH (referenced in 41 articles , 1 standard article )

Showing results 1 to 20 of 41.
Sorted by year (citations)

1 2 3 next

  1. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  2. Strichman, Ofer (ed.); Kroening, Daniel (ed.): Preface to the special issue “SI: satisfiability modulo theories” (2013)
  3. Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
  4. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  5. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  6. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  7. Babić, Domagoj; Hu, Alan J.: Approximating the safely reusable set of learned facts (2009) ioport
  8. Kroening, Daniel; Strichman, Ofer: A framework for satisfiability modulo theories (2009)
  9. Scholl, Christoph; Disch, Stefan; Pigorsch, Florian; Kupferschmid, Stefan: Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints (2009)
  10. Tiwari, Ashish: Combining equational reasoning (2009)
  11. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  12. Badban, Bahareh; Van De Pol, Jaco; Tveretina, Olga; Zantema, Hans: Generalizing DPLL and satisfiability for equalities (2007)
  13. Ganesh, Vijay; Dill, David L.: A decision procedure for bit-vectors and arrays (2007)
  14. Stump, Aaron: Imperative LF meta-programming (2007)
  15. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2006)
  16. Bhattacharya, Ritwik; German, Steven M.; Gopalakrishnan, Ganesh: Exploiting symmetry and transactions for partial order reduction of rule based specifications (2006)
  17. Conchon, Sylvain; Krstić, Sava: Strategies for combining decision procedures (2006)
  18. Currie, David; Feng, Xiushan; Fujita, Masahiro; Hu, Alan J.; Kwan, Mark; Rajan, Sreeranga: Embedded software verification using symbolic execution and uninterpreted functions (2006)
  19. Dams, Dennis R.; Namjoshi, Kedar S.: Orion: high-precision methods for static error analysis of C and C++ programs (2006)
  20. Rodeh, Yoav; Strichman, Ofer: Building small equality graphs for deciding equality logic with uninterpreted functions (2006)

1 2 3 next