TY - GEN
T1 - VeriLucid
T2 - ACM SIGCOMM 2026 Conference, SIGCOMM 2026
AU - Sonchack, John
AU - Zave, Pamela
AU - Rexford, Jennifer
N1 - Publisher Copyright: © 2026 Copyright held by the owner/author(s).
PY - 2026/8/11
Y1 - 2026/8/11
N2 - Correctness is important in data-plane programs, which run on critical infrastructure connecting millions of users. Verification helps programmers build correct software, but current data-plane tools can only check simple properties or require immense programmer effort. As a solution, this paper introduces the first verification-aware data-plane language: VeriLucid. The core idea is to unify programming and specification in one high-level language, with built-in proof automation. Integration makes it natural for programmers to use verification continuously throughout development, like unit testing but with strong guarantees. In evaluation, we show that VeriLucid requires 10X less programmer effort, in terms of lines of code, than other verification tools with comparable expressiveness.
AB - Correctness is important in data-plane programs, which run on critical infrastructure connecting millions of users. Verification helps programmers build correct software, but current data-plane tools can only check simple properties or require immense programmer effort. As a solution, this paper introduces the first verification-aware data-plane language: VeriLucid. The core idea is to unify programming and specification in one high-level language, with built-in proof automation. Integration makes it natural for programmers to use verification continuously throughout development, like unit testing but with strong guarantees. In evaluation, we show that VeriLucid requires 10X less programmer effort, in terms of lines of code, than other verification tools with comparable expressiveness.
KW - data-plane programming
KW - verification
UR - https://www.scopus.com/pages/publications/105049726791
UR - https://www.scopus.com/pages/publications/105049726791#tab=citedBy
U2 - 10.1145/3789240.3829171
DO - 10.1145/3789240.3829171
M3 - Conference contribution
T3 - SIGCOMM 2026 - Proceedings of the 2026 ACM SIGCOMM 2026 Conference
SP - 122
EP - 139
BT - SIGCOMM 2026 - Proceedings of the 2026 ACM SIGCOMM 2026 Conference
PB - Association for Computing Machinery, Inc
Y2 - 17 August 2026 through 21 August 2026
ER -