P4 Developer Days – P4Check: a P4 Verification Tool

Abstract

We present P4Check, a scalable and practical one-stop shop for verifying data planes defined in P4. P4Check combines well-proven techniques, symbolic execution, big-step semantics and model checking with a novel high-level specification language into a tool to verify properties of stateful P4 programs at both the device and network levels. We present case studies showing property verification and bug detection for real-world P4 programs and conduct experiments to quantify the performance of p4Check compared to earlier works.

Speaker

Tommaso Pacciani is a PhD candidate in Multiscale Networked Systems (MNS) at the University of Amsterdam. His research focuses on applying formal methods and language design to enable the verification of programmable networks. His additional research interests include functional programming, effect systems, and debugging.