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

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

1 2 next

  1. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  3. 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)
  4. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  5. Böhme, Sascha; Fox, Anthony C.J.; Sewell, Thomas; Weber, Tjark: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL (2011)
  6. Krishnamoorthy, Saparya; Hsiao, Michael S.; Lingappan, Loganathan: Strategies for scalable symbolic execution-driven test generation for programs (2011)
  7. Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael: Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers (2010) ioport
  8. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  9. Böhme, Sascha; Weber, Tjark: Fast LCF-style proof reconstruction for Z3 (2010)
  10. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  11. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  12. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2009)
  13. Schreiner, Wolfgang: The RISC ProofNavigator: a proving assistant for program verification in the classroom (2009)
  14. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  15. Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor: Combining theories with shared set operations (2009)
  16. Moskal, Michał: Rocket-fast proof checking for SMT solvers (2008)
  17. Narain, Sanjai; Levin, Gary; Malik, Sharad; Kaul, Vikram: Declarative infrastructure configuration synthesis and debugging (2008) ioport
  18. Sorge, Volker; Meier, Andreas; McCasland, Roy; Colton, Simon: Automatic construction and verification of isotopy invariants (2008)
  19. Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen: Verification of clock synchronization algorithms: experiments on a combination of deductive tools (2007)
  20. Kang, Eun-Young; Merz, Stephan: Predicate diagrams for the verification of real-time systems (2007)

1 2 next