Wed 17 Jun 2026 15:20 - 15:40 at Flatirons 2 - Networking and Distributed Systems Chair(s): Mae Milano

We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.

Wed 17 Jun

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

14:00 - 15:40
Networking and Distributed SystemsPLDI Research Papers at Flatirons 2
Chair(s): Mae Milano Princeton University
14:00
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:20
20m
Talk
MatchBox: A Semantic Foundation for Data Plane PortabilityDistinguished Paper
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:40
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
15:00
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:20
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