Created: 2012/11/21 16:47:39+0000

This section introduces background information on model checking. This is needed to understand the underlying implementation and how it is formalized but not the general principle.

The principle behind model checking is straight forward. It takes a model or a program and fully explores all possible executions of it. A specification is applied to each possible execution to evaluate a property. This evaluation is used to make statements about the correctness of the program and its behavior. This also allows statements to be made about concurrent programs as it can also explore all the possible ways of interleaving concurrent statements. This takes substantial computing resources particularly when exploring how concurrent statements can be interleaved.