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

by: J Burch, E Clarke, K Mcmillan, D Dill, L Hwang

(1990), pp. 1-33.

View FullText article

CiteSeer (at Penn State), CiteSeer (at MIT), CiteSeer (at Zurich), CiteSeer (at Singapore)

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

mercutio, Benet, johannsen, mccrimson, zuleger

Find related articles with these CiteULike tags

bdd, logic, modelchecking, model_checking, model-checking, no-tag, symbolic, verification

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...

@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 = {bdd, logic, model-checking, symbolic, verification}, pages = {1--33}, posted-at = {2005-03-16 23:07:08}, priority = {3}, publisher = {IEEE Computer Society Press}, title = {Symbolic Model Checking: \$10^20\$ States and Beyond}, url = {http://citeseer.ist.psu.edu/burch90symbolic.html}, year = {1990} }

RIS record

TY - CONF ID - citeulike:130316 L3 - citeulike-article-id:130316 TI - Symbolic Model Checking: $10^20$ States and Beyond T2 - Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science SP - 1 EP - 33 AD - Washington, D.C. PB - IEEE Computer Society Press 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... KW - bdd KW - logic KW - model-checking KW - symbolic KW - verification 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 -

RIS BibTeX