Symbolic Model Checking: $10^20$ States and Beyond

@inproceedings{citeulike:130316, abstract = {Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary...}, address = {Washington, D.C.}, author = {Burch, J. and Clarke, E. and Mcmillan, K. and Dill, D. and Hwang, L. }, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science}, citeulike-article-id = {130316}, keywords = {modelchecking}, pages = {1--33}, posted-at = {2005-03-17 09:33:56}, priority = {2}, publisher = {IEEE Computer Society Press}, title = {Symbolic Model Checking: \$10^20\$ States and Beyond}, url = {http://citeseer.ist.psu.edu/burch90symbolic.html}, year = {1990} }

TY - CONF ID - citeulike:130316 L3 - citeulike-article-id:130316 N2 - Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary... AD - Washington, D.C. EP - 33 TI - Symbolic Model Checking: $10^20$ States and Beyond PB - IEEE Computer Society Press T2 - Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science SP - 1 KW - modelchecking AU - Burch, J AU - Clarke, E AU - Mcmillan, K AU - Dill, D AU - Hwang, L PY - 1990/// UR - http://citeseer.ist.psu.edu/burch90symbolic.html ER -