Thread-Modular Model Checking with Iterative Refinement

Wenrui Meng (1) , Fei He (2, 1) , Bow-Yaw Wang (2) , Qiang Liu (1)

1 THU - Tsinghua University [Beijing]
2 FORMES - Formal Methods for Embedded Systems

Thread-modular analysis is an incomplete compositional technique for verifying concurrent systems. The heuristic works rather well when there is limited interaction among system components. In this paper, we develop a refinement algorithm that makes thread-modular model checking complete. Our algorithm refines abstract reachable states by exposing local information through auxiliary variables. The experiments show that our complete thread-modular model checking

Domaines: Théorie et langage formel [cs.FL]

Wenrui Meng, Fei He, Bow-Yaw Wang, Qiang Liu. Thread-Modular Model Checking with Iterative Refinement. NFM 2012 - 4th International Conference on NASA Formal Methods, Apr 2012, Norfolk, Virginia, United States. ⟨hal-00730342⟩