Cover Image
QR Code

Satisfiability Modulo Theories: Introduction and Applications.

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...

Full description

Published in:Communications of the ACM Vol. 54; no. 9; pp. 69 - 78
Main Authors: DE MOURA, LEONARDO, BJØRNER, NIKOLAJ
Format: Article
Published: Association for Computing Machinery Sep2011
Subjects:
Software verification
Computer software testing
Debugging
Mathematical logic
Boolean algebra
Mathematical formulas
Online Access:View this record in EBSCOhost
Summary: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.