Last week, the HOL4P4 formalisation of the P4 language was presented at the OOPSLA conference. HOL4P4 is a model of the P4 language written in the interactive theorem prover HOL4, which differs from existing work by its efficient and judicious scoping mechanism and fine-grained, incremental semantic style. These design choices make it easier to construct analysis tools and model concurrent phenomena using HOL4P4. The HOL4P4 formal semantics has since been used to create a practical theorem-grade verification tool for P4, which has already been presented at VSTTE.
GitHub code: link
Paper PDF: link
Authors: Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam