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

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

1 2 3 ... 5 6 7 next

  1. Orlin, James B.; Subramani, K.; Wojciechowki, Piotr: Randomized algorithms for finding the shortest negative cost cycle in networks (2018)
  2. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  3. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  4. 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)
  5. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  6. Kopczyński, Eryk; Toruńczyk, Szymon: LOIS: syntax and semantics (2017)
  7. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  8. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
  9. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  10. Zheng, Yunhui; Ganesh, Vijay; Subramanian, Sanu; Tripp, Omer; Berzish, Murphy; Dolby, Julian; Zhang, Xiangyu: Z3str2: an efficient solver for strings, regular expressions, and length constraints (2017)
  11. Á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)
  12. Ansótegui, Carlos; Bofill, Miquel; Manyà, Felip; Villaret, Mateu: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (2016)
  13. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  14. Banković, Milan: Extending SMT solvers with support for finite domain alldifferent constraint (2016)
  15. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  16. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  17. Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea: Deciding probabilistic automata weak bisimulation: theory and practice (2016)
  18. Jonáš, Martin; Strejček, Jan: Solving quantified bit-vector formulas using binary decision diagrams (2016)
  19. Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
  20. Maréchal, Alexandre; Fouilhé, Alexis; King, Tim; Monniaux, David; Périn, Michael: Polyhedral approximation of multivariate polynomials using handelman’s theorem (2016)

1 2 3 ... 5 6 7 next