State Reduction Using Reversible Rules

We reduce the state explosion problem in automatic verification of finite-state systems by automatically collapsing subgraphs of the aph into abstract states. The key idea of the method is to identify state generation rules that can be inverted. It can be used for verification of deadlock-freedom, error and invariant checking and stuttering-invariant CTL model checking.

• Type: Conference
• Year: 1996
• Where: DAC
• Authors: C. Norris Ip, David L. Dill
• Keywords: Automatic Verification, Computer Architecture, DAC 1996, State Explosion Problem, State Generation Rules