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

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

1 2 3 4 5 6 next

  1. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  2. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  3. Kopczyński, Eryk; Toruńczyk, Szymon: LOIS: syntax and semantics (2017)
  4. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  5. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  6. Á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)
  7. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  8. Banković, Milan: Extending SMT solvers with support for finite domain alldifferent constraint (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. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  11. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  12. Jonáš, Martin; Strejček, Jan: Solving quantified bit-vector formulas using binary decision diagrams (2016)
  13. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  14. 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)
  15. Monniaux, David: A survey of satisfiability modulo theory (2016)
  16. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  17. Schlachter, Uli: Petri net synthesis for restricted classes of nets (2016)
  18. Vandin, Andrea; Tribastone, Mirco: Quantitative abstractions for collective adaptive systems (2016)
  19. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  20. Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.: HYST: a source transformation and translation tool for hybrid automaton models (2015)

1 2 3 4 5 6 next