This program is tentative and subject to change.

Wed 17 Jun 2026 14:00 - 14:20 at Flatirons 2 - Networking and Distributed Systems

Match-action tables are the core abstraction underlying network packet-processing systems, from fixed-function switches to eBPF-based software dataplanes. However, their concrete syntax and semantics vary widely across programming environments, reflecting differences in hardware generations, engineering practices, and vendor design choices. This syntactic and semantic variation renders portability of match-action tables across environments a persistent challenge. This paper presents \textsc{MatchBox}, a system for translating match-action tables across heterogeneous environments. At its core is the \emph{Match Algebra}, a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, \textsc{MatchBox} introduces a static type system based on \emph{guarded functional dependencies (GFDs)} that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the \textsc{MatchBox} compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, \textsc{MatchBox} enables concise, declarative portability specifications and realizes them as compact target tables.

This program is tentative and subject to change.

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

13:40 - 15:20
Networking and Distributed SystemsPLDI Research Papers at Flatirons 2
13:40
20m
Talk
A Formally Verified Foundation for Compositional Heterogeneous Coherence
PLDI Research Papers
An Qi Zhang University of Utah, Andrés Goens TU Darmstadt, Daniel Sorin Duke University, Vijay Nagarajan University of Utah
DOI
14:00
20m
Talk
MatchBox: A Semantic Foundation for Data Plane Portability
PLDI Research Papers
Eric Hayden Campbell University of Texas at Austin, Robert Zhang University of Texas at Austin, Divyanshu Saxena University of Texas at Austin, Aditya Akella University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
14:20
20m
Talk
SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
PLDI Research Papers
Longfei Qiu Yale University, Jingqi Xiao University of Hong Kong, Ji-Yong Shin Northeastern University, Zhong Shao Yale University
DOI
14:40
20m
Talk
Implementability of Global Distributed Protocols Modulo Network Architectures
PLDI Research Papers
Elaine Li New York University, Thomas Wies New York University
DOI
15:00
20m
Talk
Weighted NetKAT: A Programming Language For Quantitative Network Verification
PLDI Research Papers
Emmanuel Suárez Acevedo Cornell University, Tiago Ferreira University College London, Kevin Batz Cornell University, Oliver Emil Bøving Technical University of Denmark, Nate Foster EPFL; Jane Street, Alexandra Silva Cornell University
DOI