Explicit state model checking
The explicit state model checker can be used for finite as well as some
infinite state systems.
The model checker terminates on systems with infinite data-domains
(such as integers) when the set of reachable states is finite, or
a counter example to the model-checked property
can be found by the state-space exploration that the model checker performs.
In addition, the model checker will abort if the input is not suitable for
model checking or if it detects a run-time error.
Last modified: Fri Jul 24 10:49:25 PDT 1998