~/talk

On Temporal Verification of Stateful P4 Programs

on YouTube 15m
Talkat NSDI '25 · 2025-04-28..04-30· [networking, security]

speakers

name:Delong Zhang
links:none on file
name:Chong Ye
links:none on file
name:Fei He
links:none on file

resources

video:https://youtu.be/j4MeKvISB-Y
slides:none on file

summary

Introduces P4LTL, a packet-processing LTL for expressing safety (e.g., no implicit drops when a register count is in-range) and liveness (per-port activation under infinite valid packets) over stateful registers, and defines a Büchi transaction that advances the spec only per-packet. Implements prototype p4tv, evaluates on nine nontrivial stateful P4 programs with 19 verification tasks, and reports p4tv solves all tasks while BF4, P4V, Vera and Acula fail or produce spurious counterexamples due to register overapproximation.

AI-written summary · about

chapters (8)

  1. 0:00Introduction
  2. 1:18SDN and P4 background
  3. 3:02Existing P4 verifier limits
  4. 5:10Stateful P4 verification challenges
  5. 6:15Modeling with P4LTL
  6. 9:11Büchi transaction verification
  7. 12:21P4TV prototype evaluation
  8. 14:31Summary

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.