Imagen de Portada
Código QR

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

Descripción completa

Publicado en:Communications of the ACM Vol. 54; no. 9; pp. 69 - 78
Autores principales: DE MOURA, LEONARDO, BJØRNER, NIKOLAJ
Formato: Artículo
Publicado: Association for Computing Machinery Sep2011
Materias:
Software verification
Computer software testing
Debugging
Mathematical logic
Boolean algebra
Mathematical formulas
Acceso en línea:Ver este registro en EBSCOhost
Sumario: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.