Skip to Main content Skip to Navigation
New interface
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 Connect in order to contact the contributor
Submitted on : Sunday, September 9, 2012 - 4:55:02 PM
Last modification on : Friday, February 4, 2022 - 3:08:43 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