[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Reverse search of the state space
- From: Matt Jennings <jen...@xxxxxxxxx>
- Date: Sun, 14 Oct 2018 18:15:07 -0700 (PDT)
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.