Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn about a groundbreaking approach to temporal verification of stateful P4 programs in this 15-minute conference presentation from NSDI '25. Discover how researchers from Tsinghua University address the limitations of existing P4 verifiers that overapproximate the stateful nature of P4 programs and prove inadequate for verifying network functions requiring stateful decision-making. Explore the innovative P4LTL specification language designed specifically for describing temporal properties of stateful P4 programs at the packet processing level, and understand the novel concept of Büchi transactions that represent the product of P4 programs and P4LTL specifications. Examine how the P4 program verification problem reduces to determining the existence of fair and feasible traces within Büchi transactions, representing the first attempt at temporal verification of stateful P4 programs at the packet processing level. Review the implementation of the p4tv prototype tool and evaluation results demonstrating its effectiveness and efficiency in temporal verification of stateful P4 programs, providing crucial insights for network programmability and verification in modern data plane programming.
