Skip to Main content Skip to Navigation
Conference papers

Compositional Verification in Action

Hubert Garavel 1 Frédéric Lang 1 Laurent Mounier 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Concurrent systems are intrinsically complex and their verification is hampered by the well-known "state-space explosion" issue. Compositional verification is a powerful approach, based on the divide-and-conquer paradigm, to address this issue. Despite impressive results, this approach is not used widely enough in practice, probably because it exists under multiple variants that make knowledge of the field hard to attain. In this article, we highlight the seminal results of Graf & Steffen and propose a survey of compositional verification techniques that exploit (or not) these results.
Complete list of metadata

Cited literature [104 references]  Display  Hide  Download
Contributor : Hubert Garavel Connect in order to contact the contributor
Submitted on : Monday, October 8, 2018 - 2:38:17 PM
Last modification on : Thursday, October 21, 2021 - 3:46:26 AM
Long-term archiving on: : Wednesday, January 9, 2019 - 3:39:02 PM


Files produced by the author(s)




Hubert Garavel, Frédéric Lang, Laurent Mounier. Compositional Verification in Action. FMICS 2018 - 23rd International Conference on Formal Methods for Industrial Critical Systems, Sep 2018, Maynooth, Ireland. pp.189-210, ⟨10.1007/978-3-030-00244-2_13⟩. ⟨hal-01890246⟩



Record views


Files downloads