Model checking is an automatic method for verifying correctness of (finite state) reactive programs with respect to temporal logic specifications. The method is algorithmic, exploiting the fixpoint characterizations of the temporal operators to permit a systematic and efficient search of the system state graph. A resulting advantage is that not only does it cater for verification of correctness, but also debugging of incorrect programs through a counter-example facility that program developers find useful. The primary limitation to model checking is the state explosion problem; a related limitation is that the basic method is only applicable to finite state programs. In this tutorial, we will introduce the basics of temporal logic, its use in describing correctness properties, and the ideas underlying efficient model checking algorithms. We discuss the use of existing model checking technology in industry, describing the use of model checking tools for such applications as hardware verification and software protocol validation. We then overview the most promising methods for ameliorating state explosion, and techniques for handling classes of infinite state and parameterized asynchronous software systems.

Model checking originated as part of Alan Emerson's dissertation work. His work also introduced the CTL branching time logic, which is widely used in industry with verification tools such as SMV, VIS, and IBM's RuleBase. The use of the Mu-calculus as a uniform formalism subsuming most commonly used temporal or modal logics of programs was proposed in 1986, along with polynomial time model checking algorithms for useful fragments of the Mu-calculus. Nowadays much of the instructor's time and energy is devoted to methods for overcoming state explosion, the chief obstacle to the more widespread application of model checking. Emerson serves on the editorial boards for ACM Transactions on Computational Logic , Formal Aspects of Computing, and Formal Methods in System Design, and is presently Bruton Centennial Professor of Computer Sciences at The University of Texas at Austin. Emerson is co-winner of the 1998 ACM Kanellakis Theory and Practice Award for his foundational role in the invention of symbolic model checking.