Book chapter
SMT-Based Model Checking
NASA Formal Methods, pp.1-1
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2012
DOI: 10.1007/978-3-642-28891-3_1
Abstract
It is widely recognized that the field of model checking owes much of its great success and impact to the use of symbolic techniques to reason efficiently about the reachable states of a hardware or software system. Traditionally, these techniques have relied on propositional encodings of transition systems and on propositional reasoning engines such asBDDs and SAT solvers. More recently, a number of these techniques have been adapted, and new ones have been devised, based instead on first-order encodings and reasoners for Satisfiability Modulo Theories (SMT).
Details
- Title: Subtitle
- SMT-Based Model Checking
- Creators
- Cesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- NASA Formal Methods, pp.1-1
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-28891-3_1
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984259407202771
Metrics
10 Record Views