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 metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00666660
Contributor : Frédéric Davesne <>
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

File

LFFP_APLAS11.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

192

Files downloads

251