PNPEq: Verification of Scheduled Conditional Behavior in Embedded Software using Petri Nets

Software for embedded systems goes through a scheduling phase where it is subjected to optimizing transformations. In such a scenario, validating the preservation of semantics across the transformation is essential. In this paper, we present PNPEq (Petri Net Program Equivalence), an ongoing work on a novel translation validation technique to handle various schedule-time conditional optimizations a...