Model checking verifies whether a given structure is a model of a given logical formula. Model checking can be applied to all kinds of logics and appropriate structures.

An important class of model checking methods have been developed for the automatic verification of formal systems. This is achieved by verifying if the structure, which is generally derived from a hardware or software design, satisfies a formal specification, typically a temporal logic formula.

The most common use for model checking is for verifying hardware designs. For software, model checking cannot be fully automatic because it may fail to prove or disprove a given property, due to undecidability.

The structure is usually given as a source code description in an industrial hardware description language or a special-purpose language. Such a program corresponds to a finite state machine (FSM), i.e., a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. The nodes represent states of a system, the edges represent possible transitions which may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution.

The main challenge in model checking is in dealing with the state space explosion problem. This occurs in systems having many components that interact with each other, or systems with data structures that can assume many different values.