A survey of satisfiability modulo theory
From MaRDI portal
Abstract: Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.
Recommendations
Cites work
- A BLAS based C library for exact linear algebra on integer matrices
- A Decision Procedure for the First Order Theory of Real Addition with Order
- A model-constructing satisfiability calculus
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Algorithms in real algebraic geometry
- An interpolating theorem prover
- Anneaux preordonnes
- Applying Linear Quantifier Elimination
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- Deciding floating-point logic with abstract conflict driven clause learning
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Fast LCF-Style Proof Reconstruction for Z3
- Generalizing DPLL to Richer Logics
- Generating non-linear interpolants by semidefinite programming
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 1234104 (Why is no real title available?)
- scientific article; zbMATH DE number 1157658 (Why is no real title available?)
- scientific article; zbMATH DE number 2151204 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- scientific article; zbMATH DE number 3408928 (Why is no real title available?)
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Lazy Abstraction with Interpolants
- Linear Programming
- Linear quantifier elimination as an abstract decision procedure
- Modular forms, a computational approach. With an appendix by Paul E. Gunnells
- Natural domain SMT: a preliminary assessment
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
- Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
- Playing in the grey area of proofs
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- Proof tree preserving interpolation
- Representing polynomials by positive linear functions on compact convex polyhedra
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Solving non-linear arithmetic
- Solving systems of polynomial inequalities in subexponential time
- Symbolic execution and program testing
- The intractability of resolution
Cited in
(38)- A framework for satisfiability modulo theories
- Theory decision by decomposition
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- Modular strategic SMT solving with \textbf{SMT-RAT}
- A practical approach to satisfiability modulo linear integer arithmetic
- \textsf{TSAT++}: an open platform for satisfiability modulo theories
- An experiment with satisfiability modulo SAT
- Taking satisfiability to the next level with Z3 (abstract)
- I-RiSC: an SMT-compliant solver for the existential fragment of real algebra
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Satisfiability modulo theories
- Lazy satisfiability modulo theories
- On the Satisfiability of Modular Arithmetic Formulae
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Engineering DPLL(T) + Saturation
- Natural domain SMT: a preliminary assessment
- Satisfiability modulo theories: an appetizer
- Satisfiability checking: theory and applications
- Precise and complete propagation based local search for satisfiability modulo theories
- Satisfiability: where Theory meets Practice (Invited Talk).
- Foundations of satisfiability modulo theories
- The MathSAT5 SMT solver
- A Tutorial on Satisfiability Modulo Theories
- Challenges in Satisfiability Modulo Theories
- An Abstract Framework for Satisfiability Modulo Theories
- Computer Aided Verification
- Satisfiability modulo linear arithmetic over a finite ring
- Bugs, moles and skeletons: symbolic reasoning for software development
- From Propositional Satisfiability to Satisfiability Modulo Theories
- Combined Satisfiability Modulo Parametric Theories
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Reasoning about vectors: satisfiability modulo a theory of sequences
- Computing optimal hypertree decompositions with SAT
- SMT sampling via model-guided approximation
- Satisfiability modulo finite fields
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
Describes a project that uses
Uses Software
This page was built for publication: A survey of satisfiability modulo theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2830018)
