CVC Lite

CVC Lite is no longer being maintained. Please visit the CVC3 web site for the current version of CVC. -------------- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.


References in zbMATH (referenced in 42 articles )

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

1 2 3 next

  1. de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
  2. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  4. Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: versat: a verified modern SAT solver (2012)
  5. Armand, Michael; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin: A modular integration of SAT/SMT solvers to Coq through proof witnesses (2011)
  6. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  8. Böhme, Sascha; Fox, Anthony C. J.; Sewell, Thomas; Weber, Tjark: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL (2011)
  9. Krishnamoorthy, Saparya; Hsiao, Michael S.; Lingappan, Loganathan: Strategies for scalable symbolic execution-driven test generation for programs (2011)
  10. Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael: Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers (2010) ioport
  11. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  12. Böhme, Sascha; Weber, Tjark: Fast LCF-style proof reconstruction for Z3 (2010)
  13. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  14. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  15. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2009)
  16. Schreiner, Wolfgang: The RISC ProofNavigator: a proving assistant for program verification in the classroom (2009)
  17. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  18. Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor: Combining theories with shared set operations (2009)
  19. Gurfinkel, Arie; Wei, Ou; Chechik, Marsha: Model checking recursive programs with exact predicate abstraction (2008)
  20. Moskal, Michał: Rocket-fast proof checking for SMT solvers (2008)

1 2 3 next