Title :
State reduction using reversible rules
Author :
Ip, C. Norris ; Dill, David L.
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
Abstract :
We reduce the state explosion problem in automatic verification of finite-state systems by automatically collapsing subgraphs of the state graph 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
Keywords :
formal verification; logic design; protocols; CTL model checking; abstract states; automatic verification; deadlock-freedom verification; finite-state systems; invariant checking; reversible rules; state explosion problem; state generation rules; state reduction; Boolean functions; Computer science; Data structures; Explosions; Formal verification; Message passing; Permission; Protocols; State-space methods; System recovery;
Conference_Titel :
Design Automation Conference Proceedings 1996, 33rd
Conference_Location :
Las Vegas, NV
Print_ISBN :
0-7803-3294-6
DOI :
10.1109/DAC.1996.545639
