Skip to Main content Skip to Navigation
Conference papers

Towards a certified Petri net model-checker

Abstract : Petri nets are widely used in the domain of automated veri cation through model-checking. In this approach, a Petri Net model of the system of interest is produced and its reachable states are computed, searching for erroneous executions. Model compilation can accelerate this analysis by generating code to explore the reachable states. This avoids the use of a xed exploration tool involving an \interpretation" of the Petri net structure. In this paper, we show how to compile Petri nets targeting the LLVM language (a high-level assembly language) and formally prove the correctness of the produced code. To this aim, we de ne a structural operational semantics for the fragment of LLVM we use.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Frédéric Davesne Connect in order to contact the contributor
Submitted on : Friday, November 29, 2013 - 4:33:40 PM
Last modification on : Tuesday, June 30, 2020 - 11:56:08 AM
Long-term archiving on: : Monday, March 3, 2014 - 1:50:38 PM


Files produced by the author(s)




Lukasz Fronc, Franck Pommereau. Towards a certified Petri net model-checker. 9th Asian Symposiium on Programming Languages and Systems (APLAS 2011), Dec 2011, Kenting, Taiwan. pp.322--336, ⟨10.1007/978-3-642-25318-8_24⟩. ⟨hal-00666660⟩



Record views


Files downloads