SMT-LIB

SMT-LIB was created with the expectation that the availability of common standards and a library of benchmarks would greatly facilitate the evaluation and the comparison of SMT systems, and advance the state of the art in the field in the same way as, for instance, the TPTP library has done for theorem proving, or the SATLIB library has done initially for SAT.


References in zbMATH (referenced in 91 articles )

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

1 2 3 4 5 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  3. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  4. Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.: Race against the teens -- benchmarking mechanized math on pre-university problems (2016)
  5. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  6. Baumgartner, Peter: SMTtoTPTP -- a converter for theorem proving formats (2015)
  7. Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe: Beagle -- a hierarchic superposition theorem prover (2015)
  8. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  9. Cok, David R.; Stump, Aaron; Weber, Tjark: The 2013 evaluation of SMT-COMP and SMT-LIB (2015)
  10. Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
  11. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A first class Boolean sort in first-order theorem proving and TPTP (2015)
  12. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  13. Beckert, Bernhard; Bruns, Daniel; Klebanov, Vladimir; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias: Information flow in object-oriented software (2014)
  14. Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei: Extensional crisis and proving identity (2014)
  15. Itzhaky, Shachar; Banerjee, Anindya; Immerman, Neil; Lahav, Ori; Nanevski, Aleksandar; Sagiv, Mooly: Modular reasoning about heap paths via effectively propositional formulas (2014)
  16. Ma, Qian; Duan, Zhenhua: Linear time-dependent constraints programming with MSVL (2014)
  17. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
  18. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  19. Stump, Aaron; Sutcliffe, Geoff; Tinelli, Cesare: StarExec: a cross-community infrastructure for logic solving (2014)
  20. Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha: Definability of accelerated relations in a theory of arrays and its applications (2013)

1 2 3 4 5 next