A Semantic Approach to Verifying Programmable Networks

As networks become more programmable, they are increasingly built around flexible software components. While this programmability enables new functionality and faster innovation, it also makes network behavior harder to reason about. In this talk, I will present a research agenda that brings ideas from formal methods to programmable networks. In particular, I will present techniques that leverage programmable-network semantics for concurrency safety, traffic monitoring, and failure recovery. More broadly, this work illustrates how semantic foundations can help bring stronger correctness guarantees to modern networked systems.

Bio
Guy Amir is a Postdoctoral Researcher at Cornell University, conducting research at the intersection of formal methods, networking, and systems. He earned his Ph.D. in 2024 from the Hebrew University of Jerusalem, where he studied AI safety, focusing on formally verifying reactive AI systems and interpreting neural networks. He holds an M.Sc. in Computer Science and a B.Sc. in Computational Biology and Computer Science, both from the Hebrew University. He has received Rothschild, Fulbright, AI-Net, and Charles Clore fellowships, as well as an ICML Spotlight and KLA Award.