veriT

veriT: An Open, Trustable and Efficient SMT-Solver. This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.


References in zbMATH (referenced in 20 articles )

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

  1. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  2. Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas: \ssfSC$^2$: satisfiability checking meets symbolic computation. (Project paper) (2016)
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  4. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  5. Bright, Curtis; Ganesh, Vijay; Heinle, Albert; Kotsireas, Ilias; Nejati, Saeed; Czarnecki, Krzysztof: mathcheck2: a SAT+CAS verifier for combinatorial conjectures (2016)
  6. Echenim, Mnacho; Peltier, Nicolas: A superposition calculus for abductive reasoning (2016)
  7. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
  8. Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers (2015)
  9. Barkati, Karim; Wang, Haisheng; Jouvelot, Pierre: Faustine: a vector faust interpreter test bed for multimedia signal processing. System description (2014)
  10. Boudou, Joseph; Woltzenlogel Paleo, Bruno: Compression of propositional resolution proofs by lowering subproofs (2013)
  11. Déharbe, David: Integration of SMT-solvers in B and Event-B development environments (2013)
  12. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  13. de Oliveira, Diego Caminha B.; Déharbe, David; Fontaine, Pascal: Combining decision procedures by (model-)equality propagation (2012)
  14. Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: versat: a verified modern SAT solver (2012)
  15. 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)
  16. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  17. Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Exploiting symmetry in SMT problems (2011)
  18. Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Compression of propositional resolution proofs via partial regularization (2011)
  19. Chaudhuri, Kaustuv; Doligez, Damien; Lamport, Leslie; Merz, Stephan: Verifying safety properties with the TLA$^ + $ proof system (2010) ioport
  20. Bouton, Thomas; Caminha B.de Oliveira, Diego; Déharbe, David; Fontaine, Pascal: veriT: An open, trustable and efficient SMT-solver (2009) ioport