@inproceedings{71ba362c9e474291871dcf71cf0bf55f,
title = "P4V: Practical verification for programmable data planes",
abstract = "We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.",
keywords = "P4, Programmable data planes, Verification",
author = "Jed Liu and Robert Soul{\'e} and William Hallahan and Han Wang and Cole Schlesinger and Calin Cascaval and Milad Sharif and Nick McKeown and Jeongkeun Lee and Nate Foster",
note = "Publisher Copyright: {\textcopyright} 2018 Copyright held by the owner/author(s).; 2018 Conference of the ACM Special Interest Group on Data Communication, ACM SIGCOMM 2018 ; Conference date: 20-08-2018 Through 25-08-2018",
year = "2018",
month = aug,
day = "7",
doi = "10.1145/3230543.3230582",
language = "English",
series = "SIGCOMM 2018 - Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication",
publisher = "Association for Computing Machinery",
pages = "490--503",
booktitle = "SIGCOMM 2018 - Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication",
}