In model checking one uses algorithmic techniques to establish the correctness of the design with respect to a given property. Model checking is based on a small number of key algorithmic ideas, tying together graph theory, automata theory, and logic. In the last few years, this area has seen a dramatic expansion of activities. Today many companies cannot wait to get the most advanced tools available, and many of them have formed R&D groups to develop model checking tools and apply them to their own designs. Unfortunately, myths abound about the computational complexity of model checking. This talk will provide an overview of model checking from the perspective of computational complexity and will explain why such complexity pose a serious barrier to the broad applicability of model checking.