@leonardo

Partition Refinement in Abstract Model Checking

, and . Theoretical Aspects of Software Engineering, 2007. TASE '07. First Joint IEEE/IFIP Symposium on, page 209--218. (2007)
DOI: 10.1109/TASE.2007.36

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.

Links and resources

Tags

community

  • @dblp
  • @leonardo
@leonardo's tags highlighted