Skip to Main content Skip to Navigation
Conference papers

Thread-Modular Model Checking with Iterative Refinement

Wenrui Meng 1 Fei He 2, 1 Bow-Yaw Wang 2 Qiang Liu 1
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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
Document type :
Conference papers
Complete list of metadata
Contributor : Fei He <>
Submitted on : Sunday, September 9, 2012 - 4:55:02 PM
Last modification on : Wednesday, June 2, 2021 - 3:39:58 AM


  • HAL Id : hal-00730342, version 1



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⟩



Record views