Taming Unbounded Distributed Systems with Modular, Bounded Verification
16/11/2021, 9am
Speaker
Abstract
Modern distributed services are typically built in a modular fashion using core distributed protocols as building blocks. The ubiquity of some of these building blocks has sparked several valiant verification efforts for them in the last decade. Oddly, there have been far fewer verification efforts that go beyond core protocols and target distributed services built on top of such core protocols. In our Discover[i ] project, we seek to develop modular, scalable, fully-automated verification approaches for distributed systems that mimic their modular design. In particular, we advocate an approach based on assuming that the underlying core protocols are verified separately and encapsulating theircomplexities within cleanly-defined abstractions.
In this talk, I will present QuickSilver, a modeling and verification framework for distributed systems built on top of verified distributed agreement protocols such as consensus. I will show how our encoding of agreement protocols facilitates decidable and scalable verification for a broad class of systems including a datastore, a lock service, a surveillance system, and several otherinteresting case studies adapted from real-world applications.
I will also briefly discuss our MANTIS project on semantics-guided inductiveprogram synthesis.
Speaker Bio
Roopsha Samanta is an Assistant Professor the Department of Computer Science at Purdue University. She leads the Purdue Formal Methods (PurForM) group and is a member of the Purdue Programming Languages (PurPL) group. Before joining Purdue in 2016, she completed her PhD at UT Austin in 2013, advised by E. Allen Emerson and Vijay K. Garg, and was a postdoctoral researcher at IST Austria from 2014-2016 with Thomas A. Henzinger. She is a recipient of a 2019 NSF CAREERaward and a 2021 Amazon Research Award.
Her research interests are in program verification, program synthesis, and concurrency. She likes to work at the intersection of formal methods and programming languages to develop frameworks to assist programmers write reliable programs. Her current research agenda is centered around two themes—formal reasoning about distributed systems and semantics-guided inductive programsynthesis.