Compositional Reasoning in Model Checking

@article{citeulike:3013019, abstract = {The main problem in model checking that prevents it from being used for verification 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 difficulty 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. This research is...}, author = {Berezin, Sergey and Campos, S\'ergio and Clarke, Edmund M. }, citeulike-article-id = {3013019}, journal = {Lecture Notes in Computer Science}, keywords = {copy, model-checking, theorem-proving}, pages = {81--102}, posted-at = {2008-07-17 04:01:21}, priority = {2}, title = {Compositional Reasoning in Model Checking}, url = {http://citeseer.ist.psu.edu/75547.html}, volume = {1536}, year = {1998} }

TY - JOUR ID - citeulike:3013019 L3 - citeulike-article-id:3013019 TI - Compositional Reasoning in Model Checking JF - Lecture Notes in Computer Science VL - 1536 SP - 81 EP - 102 N2 - The main problem in model checking that prevents it from being used for verification 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 difficulty 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. This research is... KW - copy KW - model-checking KW - theorem-proving AU - Berezin, Sergey AU - Campos, S\'ergio AU - Clarke, Edmund PY - 1998/// UR - http://citeseer.ist.psu.edu/75547.html ER -