Vendor Logo

Cornell University – Petr4

Petr4 is a formal framework that models the semantics of P4. It consists of a clean-slate definitional interpreter for P4 and a formal calculus that models the essential features of the language.

Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus approximates target-specific behaviors using non-determinism.

The Petr4 interpreter was  validated with a suite of over 750 tests from the P4 reference implementation, exercising the target interface with tests for different targets. The core calculus was validated with a proof of type-preserving termination.

Petr4 repository