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 49 articles , 1 standard article )

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

1 2 3 next

  1. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick: Optimization modulo non-linear arithmetic via incremental linearization (2021)
  2. Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal: Proofs in satisfiability modulo theories (2015)
  3. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  4. Strichman, Ofer (ed.); Kroening, Daniel (ed.): Preface to the special issue “SI: satisfiability modulo theories” (2013)
  5. 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)
  6. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  7. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  8. Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan: New results on rewrite-based satisfiability procedures (2009)
  9. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  10. Babić, Domagoj; Hu, Alan J.: Approximating the safely reusable set of learned facts (2009) ioport
  11. Kroening, Daniel; Strichman, Ofer: A framework for satisfiability modulo theories (2009)
  12. Li, Li; He, Kai-Duo; Gu, Ming; Song, Xiao-Yu: Equality detection for linear arithmetic constraints (2009)
  13. Scholl, Christoph; Disch, Stefan; Pigorsch, Florian; Kupferschmid, Stefan: Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints (2009)
  14. Tiwari, Ashish: Combining equational reasoning (2009)
  15. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  16. Nguyen, Huu Hai; Chin, Wei-Ngan: Enhancing program verification with lemmas (2008)
  17. Badban, Bahareh; Van De Pol, Jaco; Tveretina, Olga; Zantema, Hans: Generalizing DPLL and satisfiability for equalities (2007)
  18. Bonacina, Maria Paola; Echenim, Mnacho: Rewrite-based decision procedures (2007)
  19. Ganesh, Vijay; Dill, David L.: A decision procedure for bit-vectors and arrays (2007)
  20. Stump, Aaron: Imperative LF meta-programming (2007)

1 2 3 next