As described a model checker typically examines all the possible states and execution paths in a systematic and exhaustive manner in order to check if one or more properties hold. That’s how it works in theory. But in practice and for realistic systems, “all the possible states and execution paths” can be such a large number that the model checker runs out of essential system resources such as memory before it can complete its task. In fact, in the worst case, the number of states increases exponentially with every variable or thread added to the system. This state space explosion problem has been the target of a great deal of research.