A formal method to detect possible P4 specific errors

P4 is a programming language to develop data processing of networks. These kind of programs are used in network devices - like switches - to describe the way of forwarding the received packets to the proper device. Checking the correctness of these program is not an obvious task, because they can easily hide the run time errors. We are working on a method to detect violation of P4 specific properties for these programs. The method if based on a rule system, which can detect suspicious program parts and indicate the violated property to correct it easily. As a first step, we introduce the main idea, dealing with the access of invalid header and uninitialized fields with presenting it with a case study.

---

1. Track 2: Computer Science & Systems

---

2. Technical Session: 7th Workshop on Advances in Programming Languages

---

3. Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).