Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.