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

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

1 2 3 4 next

  1. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  2. Zhou, Min; He, Fei; Song, Xiaoyu; He, Shi; Chen, Gangyi; Gu, Ming: Estimating the volume of solution space for satisfiability modulo linear real arithmetic (2015)
  3. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  4. Yamagata, Yoriyuki; Kong, Weiqiang; Fukuda, Akira; Tang, Nguyen Van; Ohsaki, Hitoshi; Taguchi, Kenji: A formal semantics of extended hierarchical state transition matrices using CSP# (2014)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  6. Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
  7. Heras, Jónathan; Mata, Gadea; Romero, Ana; Rubio, Julio; Sáenz, Rubén: Verifying a plaftorm for digital imaging: a multi-tool strategy (2013)
  8. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  9. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  10. Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
  11. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  12. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  13. Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: A unified framework for DPLL(T) + certificates (2013)
  14. Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)
  15. Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela: Abstract domains for automated reasoning about list-manipulating programs with infinite data (2012)
  16. Falke, Stephan; Kapur, Deepak: Rewriting induction + linear arithmetic = decision procedure (2012)
  17. Furia, Carlo A.: A verifier for functional properties of sequence-manipulating programs (2012)
  18. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  19. Merz, Stephan; Vanzetto, Hernán: Automatic verification of TLA$^ + $ proof obligations with SMT solvers (2012)
  20. Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)

1 2 3 4 next

Further publications can be found at: