Towards a certified Petri net model-checker - Université d'Évry Access content directly
Conference Papers Year : 2012

Towards a certified Petri net model-checker


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.
Fichier principal
Vignette du fichier
LFFP_APLAS11.pdf (215.4 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00666660 , version 1 (29-11-2013)



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⟩
98 View
120 Download



Gmail Facebook Twitter LinkedIn More