The SMT-LIB Standard Version 2.0

By Clark W. Barrett, Aaron Stump, Cesare Tinelli. 2010

1,230 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/ae4ff80d08627cc4e242968fa8059d9b49bf0d55

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Deductive Software Verification – The KeY Book (2016, methodology): “the language of SMT solvers [Barrett et al., 2010] to typed first-order logic make it simple to import and export formulas from KeY’s program logic.”
Why3: Shepherd Your Herd of Provers (2011, background): “However, to facilitate writing, conditional expressions are allowed in terms, as in the following deﬁnition of absolute value: Such a construct is directly accepted by provers not making a distinction between terms and formulas ( e.g. provers supporting the SMT-LIB V2 format [3]).”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “…not just for external client software, but also for its own parser and for additional language bindings in Java and Python. cvc5 also provides a textual command-line interface (CLI), built on top of the parser, which supports SMT-LIBv2 [25], SyGuS2 [104] and TPTP [134] as input languages.”
DirectFix: Looking for Simple Program Repairs (2015, methodology): “Our trace formula is in SMT-LIB2 format [19] annotated with source code locations.”
Automated Planning and Acting (2016, methodology): “[246] use a “planning modulo theories” approach that builds on recent work on SAT modulo theories [456, 41].”
Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications (2018, methodology): “Communication with the solver is realized via the SMT-LIB standard (Barrett et al., 2015), recognized by most contemporary SMT solvers.”
A Storm is Coming: A Modern Probabilistic Model Checker (2017, background): “[43], built-in linear equations (MTBDD) CUDD [7], Sylvan [8] Bellman equations (sparse) Eigen, gmm++, built-in Bellman equations (MTBDD) CUDD, Sylvan stochastic games (sparse) built-in stochastic games (MTBDD) CUDD, Sylvan (MI)LP Gurobi [44], glpk [45] SMT Z3 [46], MathSAT [47], SMTLIB [48]”
TerpreT: A Probabilistic Programming Language for Program Induction (2016, methodology): “For this, a TerpreT instance is translated into a set of constraints in the SMT-LIB standard (Barrett et al., 2015), after which any standard SMT solver can be called.”
Introducing StarExec: a Cross-Community Infrastructure for Logic Solving (2014, background): “This includes standard input/output formats for solvers, e.g., [3, 14]; libraries of benchmark problems, e.g., [2, 6, 11, 14]; solver execution services, e.g., [12, 13, 15]; and solver competitions, e.g., [1, 4, 5, 7, 8, 9, 10].”