DocumentCode
2241790
Title
State reduction using reversible rules
Author
Ip, C. Norris ; Dill, David L.
Author_Institution
Dept. of Comput. Sci., Stanford Univ., CA, USA
fYear
1996
fDate
3-7 Jun, 1996
Firstpage
564
Lastpage
567
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference Proceedings 1996, 33rd
Conference_Location
Las Vegas, NV
ISSN
0738-100X
Print_ISBN
0-7803-3294-6
Type
conf
DOI
10.1109/DAC.1996.545639
Filename
545639
Link To Document