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

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

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