Abstract: 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. I will discuss some of the categorical tools involved in designing the semantics and the applicability of the framework.
Joint work with Emmanuel Suarez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Boving and Nate Foster.
Biography: Alexandra Silva is a theoretical computer scientist whose main research focuses on semantics of programming languages and the use of algebraic methods in network verification. Alexandra is currently a Professor at Cornell University, and she was previously a Professor at University College London. She was the recipient of an Amazon Research Award in 2023, a Cornell Bowers Research award in 2022, an ERC Consolidator in 2020, the Royal Society Wolfson Award 2019, Needham Award 2018, the Presburger Award 2017, the Leverhulme prize 2016, and an ERC starting Grant in 2015.
Hosted By: Dave Naumann, SoC Professor and Associate Dean for Research and Faculty Development
