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

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

1 2 3 4 5 next

  1. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  2. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  3. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  4. Chaudhari, Dipak L.; Damani, Om: Combining top-down and bottom-up techniques in program derivation (2015)
  5. 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)
  6. Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
  7. Wimmer, Ralf; Jansen, Nils; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd: Minimal counterexamples for linear-time probabilistic verification (2014)
  8. 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)
  9. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  10. 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)
  11. de Moura, Leonardo; Passmore, Grant Olney: The strategy challenge in SMT solving (2013)
  12. Heras, Jónathan; Mata, Gadea; Romero, Ana; Rubio, Julio; Sáenz, Rubén: Verifying a plaftorm for digital imaging: a multi-tool strategy (2013) ioport
  13. Jovanović, Dejan; Barrett, Clark: Being careful about theory combination (2013)
  14. Leino, K. Rustan M.: Automating theorem proving with SMT (2013)
  15. Lynch, Christopher; Ta, Quang-Trung; Tran, Duc-Khanh: SMELS: satisfiability modulo equality with lazy superposition (2013)
  16. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  17. Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo: Efficiently solving quantified bit-vector formulas (2013)
  18. Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: A unified framework for DPLL(T) + certificates (2013)
  19. Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)
  20. Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela: Abstract domains for automated reasoning about list-manipulating programs with infinite data (2012)

1 2 3 4 5 next


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