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

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

1 2 3 ... 5 6 7 next

  1. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  2. Orlin, James B.; Subramani, K.; Wojciechowki, Piotr: Randomized algorithms for finding the shortest negative cost cycle in networks (2018)
  3. Vale-Enriquez, Fernando; Brown, Christopher W.: Polynomial constraints and unsat cores in Tarski (2018)
  4. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  5. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  6. 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)
  7. Johansson, Moa: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (2017)
  8. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  9. Kopczyński, Eryk; Toruńczyk, Szymon: LOIS: syntax and semantics (2017)
  10. Kovács, Laura; Robillard, Simon; Voronkov, Andrei: Coming to terms with quantified reasoning (2017)
  11. Magron, Victor; Constantinides, George; Donaldson, Alastair: Certified roundoff error bounds using semidefinite programming (2017)
  12. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  13. Reynolds, Andrew; King, Tim; Kuncak, Viktor: Solving quantified linear arithmetic by counterexample-guided instantiation (2017)
  14. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
  15. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  16. 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)
  17. Á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)
  18. Ansótegui, Carlos; Bofill, Miquel; Manyà, Felip; Villaret, Mateu: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (2016)
  19. Ansótegui, Carlos; Gabàs, Joel; Levy, Jordi: Exploiting subproblem optimization in SAT-based maxsat algorithms (2016)
  20. Banković, Milan: Extending SMT solvers with support for finite domain alldifferent constraint (2016)

1 2 3 ... 5 6 7 next