Rule Generation with Model Checker
Run model-checker with unbound initial state
Instantiate state as needed
- instantiations capture assumptions about initial state
Identify those assumptions that can take the system to an unsafe state
Output set of “minimal” assumptions.