CTL model checking based on forward state traversal
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We present a CTL model checking algorithm based mainly on forward state traversal, which can check many realistic CTL properties without doing backward state traversal. This algorithm is effective in many situations where backward state traversal is more expensive than forward state traversal. We combine it with BDD-based state traversal techniques using partitioned transition relations. Experimental results show that our method can verify actual CTL properties of large industrial models which cannot be handled by conventional model checkers.Keywords
This publication has 8 references indexed in Scilit:
- Bug identification of a real chip design by symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Implicit state enumeration of finite state machines using BDD'sPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient generation of counterexamples and witnesses in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1995
- Symbolic Model CheckingPublished by Springer Nature ,1993
- Representing circuits more efficiently in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1991
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986