Reverse search of the state space

[Matt Jennings <jen...@xxxxxxxxx>]

My spec is composed of many variables and I'm not able to check it due to due to what I assume is state space explosion.   I'm wondering if for certain kinds of specs, it would be better for the model checker to start by assuming a particular invariant is violated, and work backwards looking for a path that leads back to the initial state.