BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//project/author//NONSGML v1.0//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTEND:20230502T120000Z
UID:203d81b672c3a8c3e874014d25930afa-450
DTSTAMP:19700101T120011Z
DESCRIPTION:Abstractions for Network Control Plane Verification
URL;VALUE=URI:https://www.csa.iisc.ac.in/newweb/event/450/abstractions-for-network-control-plane-verification/
SUMMARY: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.
DTSTART:20230502T120000Z
END:VEVENT
END:VCALENDAR