P4-SpecTec: A Language Mechanization Framework for P4
summary
P4-SpecTec defines a computable specification model for P4 using algorithmic inference rules (a constrained Wasm-SpecTec–style meta language), mechanizes syntax and static semantics in ~8,000 lines, and derives a working type checker that passes >99% of positive tests and >98% of negative tests. It auto-generates 248 generated negative tests and uncovers 26 previously unknown bugs (including soundness issues). Planned backends include parser, interpreter and human-readable spec output.
AI-written summary · about
chapters (10)
- 0:00P4-SpecTec framework
- 1:03Mechanization need for P4
- 4:14Spec model as single source
- 5:58WebAssembly mechanization lessons
- 10:55Mechanizing P4 challenges
- 13:27P4 algorithmic inference rules
- 18:47Executing P4 spec model
- 19:50P4-SpecTec ecosystem benefits
- 22:17Future P4 toolchain adoption
- 22:44Q&A
related talks
26mSpecTec, a Single Source of Truth
27mPetr4: Formal Foundations for P4 Data Planes
19mHOL4P4: mechanized small-step semantics for P4
22mP4-Based Automated Reasoning (P4-BAR) using Symbolic Execution
22mDependently-Typed Data Plane Programming
18mP4Cub: A Little Language for Big Routers
01h 02mProgramming Language Research for Technical and Social Good: What PL Can Do for Good?
15mOn Temporal Verification of Stateful P4 Programs