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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 56 articles )

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

1 2 3 next