Satisfiability Modulo Theories: Introduction and Applications. - DE MOURA, LEONARDO; BJØRNER, NIKOLAJ (Communications of the ACM, 2011)
The article discusses Satisfiability Modulo Theories (SMT) solvers, which are said to be the core of many tools for program analysis, testing, and verification. The topics of constraint satisfaction, propositional satisfiability, and Boolean variables are addressed. SMT solvers are able to check the satisfiability of logical formulas on a scale orders of magnitude beyond custom ad hoc solvers. Their use in software engineering tasks such as case analysis, static analysis, and modeling is also described.