Seminars

View all Seminars  |  Download ICal for this event

Abstractions for Network Control Plane Verification

Series: CSA Distinguished Lecture

Speaker: Aarti Gupta

Date/Time: May 02 11:30:00

Location: CSA Seminar Hall (Room No. 254, First Floor)

Abstract:
The network control plane is a complex distributed system that runs various protocols for exchanging messages between routers and selecting paths for routing traffic. Errors in control plane configurations can lead to expensive outages or critical security breaches, leading to great interest in applying formal methods to ensure correctness. Although verification approaches based on use of Satisfiability Modulo Theory (SMT) solvers are general and powerful, they face scalability challenges. I will describe our recent work on key abstractions and modular assume-guarantee reasoning that have enabled our SMT-based approach to successfully handle large-sized networks (with several thousands of routers), similar to those in operation in modern data centers.

This talk describes joint work with Ryan Beckett, Ratul Mahajan, Divya Raghunathan, Timothy Alberdingk Thijm, and David Walker.

Speaker Bio:
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 served on the technical program committees of many leading conferences, and is currently serving on the Steering Committee of the Computer Aided Verification (CAV) Conference. She has received several Best Paper Awards from leading conferences and journals and has been recognized as an ACM Fellow.

Host Faculty: Deepak DSouza