are widely used in the domain of automated verification through
. In this approach, a Petri Net model of the system of interest is produced and its reachable states are computed, searching for erroneous executions.
can accelerate this analysis by generating code to explore the reachable states. This avoids the use of a fixed exploration tool involving an “interpretation” of the Petri net structure. In this paper, we show how to compile Petri nets targeting the
(a high-level assembly language) and formally prove the
of the produced code. To this aim, we define a
structural operational semantics
for the fragment of LLVM we use.