Satisfiability Modulo Theories

By Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli. 2009

1,863 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Management Science and Operations Research

How researchers see this paper

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

In Artificial Intelligence

In Management Science and Operations Research

Citations in the corpus

Syntax-guided synthesis (2013, background): “An SMT solver determines the truth of a given logical formula built from typed variables, logical connectives, and typical operations such as arithmetic and array accesses (see [1], [2]).”
Output Range Analysis for Deep Feedforward Neural Networks (2018, methodology): “(b) We do not rely on existing Satisfiability-Modulo Theory (SMT) solvers [2].”
Component Caching in Hybrid Domains with Piecewise Polynomial Densities (2016, methodology): “In the recent years, driven by SMT technology (Barrett et al. 2009), diverse applications from veriﬁcation in hybrid systems (Chistikov, Dimitrova, and Majumdar 2015) to privacy (Fredrikson and Jha 2014) to inference in hybrid graphical models (Belle, Passerini, and Van den Broeck 2015) re-sort to…”
A Survey of Symbolic Execution Techniques (2016, background): “he symbols of a formula that makes it true. Although SAT is a well-known NP-complete problem, recent advances have moved the boundaries for what is intractable when it comes to practical applications [37]. Observethatsomeproblemsaremorenaturallydescribedwithlanguagesthataremoreexpressive than the on”
Probabilistic Inference in Hybrid Domains by Weighted Model Integration (2015, methodology): “For our purposes, we also need the notion of formula abstraction and refinement [Barrett et al., 2009].”
Hashing-Based Approximate Probabilistic Inference in Hybrid Domains (2015, methodology): “Standard first-order models can be used to formulate SMT; see Barrett et al. (2009) for details.”
Scheduling Real-Time Communication in IEEE 802.1Qbv Time Sensitive Networks (2016, neutral): “Satisfiability Modulo Theories (SMT) are designed to determine the satisfiability of first-order logical formulas against certain background theories like linear integer arithmetic (LA(Z)) or bit-vectors (BV) [3, 29].”
Safe Control With Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control (2022, background): “satisfiability to include statements involving real numbers [32].”
Symbolic execution for software testing: three decades later (2013, methodology): “At the other end are systems like EXE [10], and more recently KLEE [8] and SAGE [15] that model pointers using the theory of arrays with selections and updates implemented by solvers like STP [16] or Z3 [14].”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “This relates clasp to SMT [10] techniques, applying “theory propagation” (cf.”
Algorithms for Verifying Deep Neural Networks (2019, methodology): “Some of these methods call Boolean satisfiability (SAT) or satisfiability modulo theories (SMT) solvers [3] to verify networks with only ReLU activations.”
Leveraging linear and mixed integer programming for SMT (2014, background): “The core SMT problem is to determine whether a first order formula φ is satisfiable with respect to a fixed first order theory T [2].”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, background): “The Satisfiability Modulo Theories problem, or SMT, is an extension of Boolean Satisfiability where the goal is to check the satisfiability of an SMT formula with respect to a background theory T [90, 104, 20].”
The SMT-LIB Standard Version 2.0 (2010, background): “Satisfiability Modulo Theories (SMT) is a growing area of automated deduction with many important applications, especially in static analysis and system verification [2].”
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation (2019, background): “Rather than continuing the race with adversaries, formal verification (Baier and Katoen, 2008; Barrett and Tinelli, 2018; Katz et al., 2017) offers a different approach: it aims at providing provable guarantees to a given model specification.”
The nuXmv Symbolic Model Checker (2014, methodology): “To analyze such kind of designs, we integrated in NUXMV several new verification algorithms based on Satisfiability Modulo Theory (SMT) [18] and on abstraction, or combination of abstraction with other techniques.”