Model checking is a computer-aided verification method developed to formally verify the correct functioning of a system design model by examining all of its possible behaviours. The models used in model checking are quite similar to those used in simulation, as basically the model must describe the behaviour of the system design for all sequences of inputs. However, unlike simulation, model checkers examine the behaviour of the system design with all input sequences and compare it with the system specification.

In model checking, at least in principle, the analysis can be fully automated with computer-aided tools. The specification is expressed in a suitable specification language, temporal logics being a prime example, describing the allowed behaviours of a system. Given a model and a specification as inputs, a model checking algorithm decides whether the system violates its specification or not. If none of the behaviours of the system violate the given specification, the (model of the) system is correct. Otherwise, the model checker will automatically give a counter-example execution of the system demonstrating why the property is violated.