Barnard Distinguished Lecture in Computer Science: Aarti Gupta (Princeton University)
Speaker: Aarti Gupta (Princeton University)
Title: Ensuring Network Correctness: Scaling Automated Verification
The seminar will be available for Zoom participation. For those attending in person, a reception will follow the talk.
Networks form an essential component of the computing infrastructure that interconnects the world and delivers immensely useful services in modern society. It is important to ensure their correctness, since bugs in network configurations can lead to expensive outages and critical security breaches. However, this is a challenging problem due to the growing complexity of configuration code and network designs. The last decade has seen tremendous advances in formal verification of networks that can find subtle buggy scenarios, which are often missed by methods based on testing or simulation. In this talk, I will describe our work on automated verification of distributed network control planes, where we reason about all possible routing behaviors that emerge from the configurations of routing protocols, to support checking a rich set of correctness properties such as reachability, fault tolerance, and router equivalence. The talk will focus on domain insights that enable effective formulation of the verification problems, and domain-based abstractions that further scale up verification on large-sized networks similar to those used in modern data centers.
This talk describes joint work with Ryan Beckett, Ratul Mahajan, Divya Raghunathan, and David Walker.
Aarti Gupta is a Professor in the Department of Computer Science at Princeton University. She received a PhD in Computer Science from Carnegie Mellon University. Her research interests are in the areas of formal verification of programs and systems, automatic decision procedures, and electronic design automation. She has received several Best Paper Awards from leading conferences and journals, and has been recognized as an ACM Fellow. She is currently serving on the Steering Committee of the Computer Aided Verification (CAV) Conference.
