Compositional reasoning in model checking Export

@inproceedings{citeulike:3486483, abstract = {Abstract. The main problem in model checking that prevents it from being used for veri cation of large systems is the state explosion problem. This problem often arises from combining parallel processes together. Many techniques have been proposed to overcome this di culty and, thus, increase the size of the systems that model checkers can handle. We describe several compositional model checking techniques used in practice and show a few examples demonstrating their performance. 1}, author = {Berezin, Sergey and Campos, Sergio and Clarke, Edmund M.}, booktitle = {In Proc. COMPOS}, citeulike-article-id = {3486483}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.8791}, keywords = {agdaspin, assume-gurantee-reasoning, model-checking}, pages = {81--102}, posted-at = {2008-11-07 03:34:50}, priority = {2}, title = {Compositional reasoning in model checking}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.8791}, year = {1998} }

TY - CONF ID - citeulike:3486483 L3 - citeulike-article-id:3486483 N2 - Abstract. The main problem in model checking that prevents it from being used for veri cation of large systems is the state explosion problem. This problem often arises from combining parallel processes together. Many techniques have been proposed to overcome this di culty and, thus, increase the size of the systems that model checkers can handle. We describe several compositional model checking techniques used in practice and show a few examples demonstrating their performance. 1 EP - 102 TI - Compositional reasoning in model checking T2 - In Proc. COMPOS SP - 81 KW - agdaspin KW - assume-gurantee-reasoning KW - model-checking AU - Berezin, Sergey AU - Campos, Sergio AU - Clarke, Edmund PY - 1998/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.8791 ER -