PLDI 2026 (series) / PLDI Research Papers /
Weighted NetKAT: A Programming Language For Quantitative Network Verification
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 JunDisplayed time zone: Mountain Time (US & Canada) change
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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Implementability of Global Distributed Protocols Modulo Network Architectures PLDI Research Papers DOI | ||
15:20 20mTalk | 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 | ||