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
Type de document :
Communication dans un congrès
NFM 2012 - 4th International Conference on NASA Formal Methods, Apr 2012, Norfolk, Virginia, United States. 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00730342
Contributeur : Fei He <>
Soumis le : dimanche 9 septembre 2012 - 16:55:02
Dernière modification le : mercredi 10 octobre 2018 - 14:28:10

Identifiants

  • HAL Id : hal-00730342, version 1

Collections

Citation

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. 2012. 〈hal-00730342〉

Partager

Métriques

Consultations de la notice

179