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 41 to 60 of 85.
Sorted by year (citations)
  1. Loup, Ulrich; Ábrahám, Erika: I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (2011)
  2. Nguyen, Thi Minh Tuyen; Marché, Claude: Hardware-dependent proofs of numerical programs (2011)
  3. Siegel, Stephen F.; Zirkel, Timothy K.: Collective assertions (2011)
  4. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  5. Sitaraman, Murali; Adcock, Bruce; Avigad, Jeremy; Bronish, Derek; Bucci, Paolo; Frazier, David; Friedman, Harvey M.; Harton, Heather; Heym, Wayne; Kirschenbaum, Jason; Krone, Joan; Smith, Hampton; Weide, Bruce W.: Building a push-button RESOLVE verifier: progress and challenges (2011) ioport
  6. Ahrendt, Wolfgang; Beckert, Bernhard; Giese, Martin; Rümmer, Philipp: Practical aspects of automated deduction for program verification (2010) ioport
  7. Ayad, Ali; Marché, Claude: Multi-prover verification of floating-point programs (2010)
  8. Baader, Franz; Beckert, Bernhard; Nipkow, Tobias: Deduktion: von der Theorie zur Anwendung (2010) ioport
  9. Brummayer, Robert; Järvisalo, Matti: Testing and debugging techniques for answer set solver development (2010)
  10. Butelle, Franck; Hivert, Florent; Mayero, Micaela; Toumazet, Frédéric: Formal proof of SCHUR conjugate function (2010)
  11. Dillig, Isil; Dillig, Thomas; Aiken, Alex: Small formulas for large programs: on-line constraint simplification in scalable static analysis (2010)
  12. Goldberg, Benjamin: Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli (2010)
  13. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  14. Korovin, Konstantin; Sticksel, Christoph: iProver-Eq: an instantiation-based theorem prover with equality (2010)
  15. Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas: Building a calculus of data structures (2010)
  16. Leino, K. Rustan M.: Dafny: an automatic program verifier for functional correctness (2010)
  17. Sherman, Elena; Garvin, Brady J.; Dwyer, Matthew B.: A slice-based decision procedure for type-based partial orders (2010)
  18. Amjad, Hasan; Bornat, Richard: Towards automatic stability analysis for rely-guarantee proofs (2009)
  19. Armando, Alessandro; Bonacina, Maria Paola; Ranise, Silvio; Schulz, Stephan: New results on rewrite-based satisfiability procedures (2009)
  20. Avigad, Jeremy; Dean, Edward; Mumma, John: A formal system for Euclid’s Elements (2009)

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