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 55 articles )

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

1 2 3 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
  3. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  4. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  5. Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal: Proofs in satisfiability modulo theories (2015)
  6. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  8. Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: \textttversat: a verified modern SAT solver (2012)
  9. 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)
  10. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  11. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  12. Böhme, Sascha; Fox, Anthony C. J.; Sewell, Thomas; Weber, Tjark: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL (2011)
  13. Krishnamoorthy, Saparya; Hsiao, Michael S.; Lingappan, Loganathan: Strategies for scalable symbolic execution-driven test generation for programs (2011)
  14. Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael: Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers (2010) ioport
  15. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  16. Böhme, Sascha; Weber, Tjark: Fast LCF-style proof reconstruction for Z3 (2010)
  17. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  18. Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan: New results on rewrite-based satisfiability procedures (2009)
  19. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  20. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2009)

1 2 3 next