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

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

1 2 next

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  3. Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
  4. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  5. Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)
  6. Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
  7. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  8. Á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: \textsfSC(^2): satisfiability checking meets symbolic computation. (Project paper) (2016)
  9. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  10. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  11. Bright, Curtis; Ganesh, Vijay; Heinle, Albert; Kotsireas, Ilias; Nejati, Saeed; Czarnecki, Krzysztof: \textscmathcheck2: a SAT+CAS verifier for combinatorial conjectures (2016)
  12. Echenim, Mnacho; Peltier, Nicolas: A superposition calculus for abductive reasoning (2016)
  13. Kremer, Gereon; Corzilius, Florian; Ábrahám, Erika: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic (2016)
  14. Abraham, Erika: Building bridges between symbolic computation and satisfiability checking (2015)
  15. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Decision procedures for flat array properties (2015)
  16. Barrett, Clark; de Moura, Leonardo; Fontaine, Pascal: Proofs in satisfiability modulo theories (2015)
  17. Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers (2015)
  18. Barkati, Karim; Wang, Haisheng; Jouvelot, Pierre: Faustine: a vector faust interpreter test bed for multimedia signal processing. System description (2014) ioport
  19. Boudou, Joseph; Woltzenlogel Paleo, Bruno: Compression of propositional resolution proofs by lowering subproofs (2013)
  20. Déharbe, David: Integration of SMT-solvers in B and Event-B development environments (2013)

1 2 next