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.
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
We present Vera, a tool that verifies P4 programs using symbolic execution. Vera automatically uncovers a number of common bugs including parsing/deparsing errors, invalid memory accesses, loops and tunneling errors, among others. Vera can also be used to verify user-specified properties in a novel language we call NetCTL. To enable scalable, exhaustive verification of P4 program snapshots, Vera automatically generates all valid header layouts and uses a novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes between 5s-15s to track the execution of a purely symbolic packet in the largest P4 program currently available (6KLOC) and can compute SEFL model updates in milliseconds. Vera can also explore multiple concrete dataplanes at once by allowing the programmer to insert symbolic table entries; the resulting verification highlights possible control plane errors. We have used Vera to analyze many P4 programs including the P4 tutorials, P4 programs in the research literature and the switch code from https://p4.org. Vera has found several bugs in each of them in seconds/minutes.
How it got here
How it got here
agent via openalex
Added
2026-10-28 21:17 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{stoenescu2018debugging,
title = {Debugging P4 programs with vera},
author = {Radu Stoenescu and Dragoș Dumitrescu and Matei Popovici and Lorina Negreanu and Costin Raiciu},
year = {2018},
journal = {ACM SIGCOMM Conference (SIGCOMM)},
pages = {518--532},
doi = {10.1145/3230543.3230548},
}