Abstract: Model checking is a mechanical, ``pushbutton'' technique for deciding whether a model of an executing system has a logical property (e.g., deciding whether a system of n-processes and m-resources avoids starvation). But what are the forms of models that can be mechanically checked? What logical properties can be checked? And how is the checking implemented? This talk surveys the answers to these questions.
By its very nature, a model must be an abstraction of the concrete, executing system that it describes. The talk concludes with an explanation of what it means for a model to be a correct abstraction of a concrete system and how such an abstraction fundamentally limits the form of properties one can mechanically model check.