[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Reverse search of the state space

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.