cvc3

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.


References in zbMATH (referenced in 85 articles )

Showing results 21 to 40 of 85.
Sorted by year (citations)
  1. Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela: Abstract domains for automated reasoning about list-manipulating programs with infinite data (2012)
  2. Falke, Stephan; Kapur, Deepak: Rewriting induction + linear arithmetic = decision procedure (2012)
  3. Furia, Carlo A.: A verifier for functional properties of sequence-manipulating programs (2012) ioport
  4. Hatcliff, John; Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  5. Merz, Stephan; Vanzetto, Hernán: Automatic verification of TLA(^ + ) proof obligations with SMT solvers (2012)
  6. Shved, P. E.; Mutilin, V. S.; Mandrykin, M. U.: Experience of improving the BLAST static verification tool (2012)
  7. Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
  8. Bersani, Marcello M.; Demri, Stéphane: The complexity of reversal-bounded model-checking (2011)
  9. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  10. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  11. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  12. Bobot, François; Paskevich, Andrei: Expressing polymorphic types in a many-sorted language (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. Böhme, Sascha; Moskal, Michał: Heaps and data structures: a challenge for automated provers (2011)
  15. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  16. Cimatti, A.; Griggio, A.; Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories (2011)
  17. Dillig, Isil; Dillig, Thomas; Aiken, Alex: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers (2011)
  18. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  19. Gladisch, Christoph D.: Satisfiability solving and model generation for quantified first-order logic formulas (2011)
  20. Jovanović, Dejan; Barrett, Clark: Sharing is caring: combination of theories (2011)

Further publications can be found at: http://www.cs.nyu.edu/acsys/cvc3/publications.html