Month: October 2024

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 … Continue reading “P4 semantics presented at OOPSLA 2024”

In a recent paper, we show how to formally verify P4 code using the interactive theorem prover (ITP) HOL4. The method creates an end-to-end proof entirely inside the logic of the ITP, and is applicable to real P4 programs by using the import tool of HOL4P4. To gain efficiency when symbolically executing large programs, multiple … Continue reading “HOL4P4 symbolic execution presented at VSTTE 2024”