The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Uncovering Bugs in P4 Programs with Assertion-based Verification
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.
How it got here
How it got here
agent via openalex
Added
2026-10-28 21:09 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{freire2018uncovering,
title = {Uncovering Bugs in P4 Programs with Assertion-based Verification},
author = {Lucas Freire and Miguel Neves and Lucas dos Santos Leal and Kirill Levchenko and Alberto Egon Schaeffer-Filho and Marinho Pilla Barcellos},
year = {2018},
journal = {Symposium on SDN Research},
pages = {1--7},
doi = {10.1145/3185467.3185499},
}