A Survey of Satisfiability Modulo Theory
David Monniaux
TL;DR
This survey provides a comprehensive overview of Satisfiability Modulo Theory (SMT), covering its core techniques, theoretical foundations, and applications in automated software analysis.
Contribution
It offers a detailed synthesis of SMT methods, including DPLL(T), natural domain approaches, and their use in software verification, highlighting recent developments and challenges.
Findings
Explains the combination of propositional satisfiability with decision procedures.
Describes the role of quantifiers and Craig interpolants in SMT.
Highlights applications of SMT solvers in automated software analysis.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Reliability and Analysis Research