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

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

1 2 3 ... 6 7 8 next

  1. Bansal, Kshitij; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare: Reasoning with finite sets and cardinality constraints in SMT (2018)
  2. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  3. Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon: Superposition with datatypes and codatatypes (2018)
  4. Brandl, Florian; Brandt, Felix; Eberl, Manuel; Geist, Christian: Proving the incompatibility of efficiency and strategyproofness via SMT solving (2018)
  5. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  6. Echenim, Mnacho; Peltier, Nicolas; Sellami, Yanis: A generic framework for implicate generation modulo theories (2018)
  7. Gleiss, Bernhard; Kovács, Laura; Robillard, Simon: Loop analysis by quantification over iterations (2018)
  8. Gupta, Shubhani; Saxena, Aseem; Mahajan, Anmol; Bansal, Sorav: Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition (2018)
  9. Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)
  10. König, Barbara; Nederkorn, Maxime; Nolte, Dennis: CoReS: a tool for computing core graphs via SAT/SMT solvers (2018)
  11. Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A foolish encoding of the next state relations of imperative programs (2018)
  12. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  13. Orlin, James B.; Subramani, K.; Wojciechowki, Piotr: Randomized algorithms for finding the shortest negative cost cycle in networks (2018)
  14. Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark: Datatypes with shared selectors (2018)
  15. Vale-Enriquez, Fernando; Brown, Christopher W.: Polynomial constraints and unsat cores in \textscTarski (2018)
  16. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  17. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  18. 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 \textsfAProVE (2017)
  19. Johansson, Moa: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (2017)
  20. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)

1 2 3 ... 6 7 8 next