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).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tinelli, C. (2012). SMT-Based Model Checking. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)