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...
| Publicado en: | Communications of the ACM Vol. 54; no. 9; pp. 69 - 78 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Sep2011
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=67134750&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 67134750 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Sep2011 vid: 54 iid: 9 pid: 68 pub: Association for Computing Machinery artinfo: ui: 67134750 10.1145/1995376.1995394 ppf: 69 ppct: 9 formats: tig: atl: Satisfiability Modulo Theories: Introduction and Applications. aug: au: DE MOURA, LEONARDO BJØRNER, NIKOLAJ affil: Senior researcher, Software Reliability Research group, Microsoft Research, Redmond, WA Senior researcher, Foundations of Software Engineering group, Microsoft Research, Redmond, WA su: Software verification Computer software testing Debugging Mathematical logic Boolean algebra Mathematical formulas sug: subj: Software verification Computer software testing Debugging Mathematical logic Boolean algebra Mathematical formulas ab: 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2011 holdings: @attributes: islocal: N |
|---|