Model Checking a Program: The operation of a model checker can be described in terms of the familiar metaphor of searching a graph (Figure shown below). The nodes of the graph represent the states of the program and the links connecting the nodes represent state changes or transitions. Branch points in the graph represent choices resulting from, for example, scheduling decisions or different input values, which can produce multiple options as to the next state to be considered by the model checker.
The state of a program can be described as the bindings of variables and data members to values, the value of the program counter representing the instruction being executed, and the information identifying the current thread of execution. The state of a program changes over time. The state graph represents the state space of the program as a whole—the collection of all possible program states and transitions.
A model checker essentially tries to cover every state in the state space and follow all the transitions, covering every state reachable by any execution path.
Explicit state model checkers support a state storage mechanism which allows them to remember the previous states that they have visited. Once a leaf state or previously visited state has been reached, the model checker can backtrack and try the other choices that could have been taken instead. Thisallows the model checker to be systematic and thorough in covering the entire state space while checking the properties of interest.