Petr4
Formal semantics and mechanized verification for P4 data plane programs
Petr4 provides a formal operational semantics for the P4 language, mechanized in the Coq proof assistant. It includes a reference interpreter for executing P4 programs and serves as the foundation for verified compilation, test generation (P4Testgen), and program analysis tools such as P4Cub.
Formal MethodsNetworkProtocol
Maturity
Support
C4DT
Lab
Maturity
Support
C4DT
Lab
The Networked Systems Abstractions Lab (LASeR) develops programming languages and formal reasoning tools for networked systems. The lab creates expressive languages to specify network behavior, develops verification techniques to confirm correctness against formal specifications, and engineers practical implementations that make sophisticated abstractions feasible. Notable contributions include algebraic frameworks (NetKAT and GKAT) and domain-specific languages for programmable network hardware (P4).
This page was last edited on 2026-04-28.
This page was last edited on 2026-04-28.