2026/08/03 by Jort van Leenen, Tobias Kappé
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.1007/978-3-032-32519-8_11
published as In proceedings of CAV 2026 (1), pp 198-211
arxiv created 2026/08/03 · arxiv updated 2026/08/04
P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool's implementation and evaluate its usability in networking contexts.