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

Showing results 1 to 17 of 17.
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. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
  5. Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers (2015)
  6. Barkati, Karim; Wang, Haisheng; Jouvelot, Pierre: Faustine: a vector faust interpreter test bed for multimedia signal processing. System description (2014)
  7. Boudou, Joseph; Woltzenlogel Paleo, Bruno: Compression of propositional resolution proofs by lowering subproofs (2013)
  8. Déharbe, David: Integration of SMT-solvers in B and Event-B development environments (2013)
  9. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  10. de Oliveira, Diego Caminha B.; Déharbe, David; Fontaine, Pascal: Combining decision procedures by (model-)equality propagation (2012)
  11. Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin: versat: a verified modern SAT solver (2012)
  12. 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)
  13. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  14. Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Exploiting symmetry in SMT problems (2011)
  15. Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Compression of propositional resolution proofs via partial regularization (2011)
  16. Chaudhuri, Kaustuv; Doligez, Damien; Lamport, Leslie; Merz, Stephan: Verifying safety properties with the TLA$^ + $ proof system (2010) ioport
  17. Bouton, Thomas; Caminha Oliveira, Diego; Déharbe, David; Fontaine, Pascal: veriT: An open, trustable and efficient SMT-solver (2009) ioport