%0 Conference Paper %1 pu_07_partition %A Pu, Fei %A Zhang, Wenhui %B Theoretical Aspects of Software Engineering, 2007. TASE '07. First Joint IEEE/IFIP Symposium on %D 2007 %J Theoretical Aspects of Software Engineering, 2007. TASE '07. First Joint IEEE/IFIP Symposium on %K 2007 refinement model_checking %P 209--218 %R 10.1109/TASE.2007.36 %T Partition Refinement in Abstract Model Checking %U http://dx.doi.org/10.1109/TASE.2007.36 %X Model checking has been successfully applied to system verification. However, in model checking, the state explosion problem occurs when one checks systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper describes a technique to decompose a model checking problem into sub-problems by partitioning the search space. The partitioning is based on the usage of extra variables remembering the history of non-deterministic choices in the model. Furthermore, the search space can be partitioned stepwise in order to get better reduction. Finally, the partition-refinement paradigm is extended to the setting of abstract systems. We show how the partition-based approach used in abstract model checking can improve the efficiency of verification with respect to the requirement of memory by illustrating an application example.

@inproceedings{pu_07_partition, abstract = {Model checking has been successfully applied to system verification. However, in model checking, the state explosion problem occurs when one checks systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper describes a technique to decompose a model checking problem into sub-problems by partitioning the search space. The partitioning is based on the usage of extra variables remembering the history of non-deterministic choices in the model. Furthermore, the search space can be partitioned stepwise in order to get better reduction. Finally, the partition-refinement paradigm is extended to the setting of abstract systems. We show how the partition-based approach used in abstract model checking can improve the efficiency of verification with respect to the requirement of memory by illustrating an application example.}, added-at = {2009-02-11T20:53:29.000+0100}, author = {Pu, Fei and Zhang, Wenhui}, biburl = {https://www.bibsonomy.org/bibtex/234aee7109b960ae5d6b6b886c702742a/leonardo}, booktitle = {Theoretical Aspects of Software Engineering, 2007. TASE '07. First Joint IEEE/IFIP Symposium on}, citeulike-article-id = {2505038}, doi = {10.1109/TASE.2007.36}, interhash = {852a7529c0cf8e6cc850bab175e4a36d}, intrahash = {34aee7109b960ae5d6b6b886c702742a}, journal = {Theoretical Aspects of Software Engineering, 2007. TASE '07. First Joint IEEE/IFIP Symposium on}, keywords = {2007 refinement model_checking}, pages = {209--218}, posted-at = {2008-03-11 00:27:17}, priority = {2}, timestamp = {2009-02-11T20:53:29.000+0100}, title = {Partition Refinement in Abstract Model Checking}, url = {http://dx.doi.org/10.1109/TASE.2007.36}, year = 2007 }