[FM-India] IARCS Verification Seminar Series -- Talk by Aarti Gupta on June 7 at 1900 hrs IST

VSS IARCS vss.iarcs at gmail.com
Mon Jun 6 11:35:52 IST 2022


Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Aarti Gupta, a Professor in the Department of Computer Science at Princeton
University. The talk is scheduled on Tuesday, June 7, at 1900 hrs IST (add
to Google calendar
<https://calendar.google.com/event?action=TEMPLATE&tmeid=NTZ1OHE4azk0dGE1dTRtNnRucXYxbGEyazcgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com>
).

The details of the talk can be found on the webpage (
https://fmindia.cmi.ac.in/vss/), and also appended to the body of this
email.

The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.

All are welcome to join.


Best regards,
Deepak, Madhukar, Rahul, Srivathsan

=============================================================

Title: Formal Verification of Distributed Network Control Planes

Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: The control plane in many networks is a complex distributed
system that runs various protocols for exchanging messages between routers
and selecting paths for routing traffic. Errors in its configuration can
lead to expensive outages or critical security breaches. The last decade
has seen tremendous advances in applying formal methods to ensure
correctness. In this talk, I will describe our efforts that started with a
general-purpose symbolic model of the behavior of a network control plane.
We encoded the stable states of a network as a satisfying assignment to a
logic formula, and leveraged Satisfiability Modulo Theory (SMT) solvers to
verify a wide variety of network correctness properties including
reachability, fault-tolerance, router equivalence, and load balancing.
Although this approach is very general and powerful, and works well for
small-sized networks (a few hundred routers), there are scalability
challenges. To address these, we embarked on a series of improvements that
use key abstractions (symmetry abstractions, nondeterministic routing),
abstract interpretation, and modular assume-guarantee reasoning. I will
describe how these techniques successfully handle large-sized networks
(several thousands of routers) that are in operation in modern data
centers.

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.


More information about the FMIndia mailing list