[Pl-seminar] Short-notice announcement: this Thursday: Roopsha Samanta/Purdue Univ.: Component-based Parameterized Reasoning for Distributed Applications

[Thomas Wahl]

The talk is somewhat early, but this was a short-notice arrangement (this Thursday!), so this is the best we could do.

-----------------------------------------------

Speaker: Roopsha Samanta, Purdue Univ.
Date:    Thursday, March 14
Time:    9:30am
Place:   WVH 366
Title:   Discover[i]: Component-based Parameterized Reasoning for Distributed Applications

Distributed systems are hard to get right. There have been many notable
efforts in formal reasoning for distributed systems: these efforts have
focused on language design, automated or semi-automated verification,
and, more recently, on automated synthesis for systems with a fixed
number of processes. Our Discover[i] project seeks to automate aspects
of programming distributed applications by developing new foundations,
algorithms and tools for synthesis/verification of distributed
applications built using (verified) components and parameterized by the
number of processes.

In this talk, I will present an approach for parameterized synthesis of
coordination for distributed systems that use consensus protocols, such
as Paxos, as a building block to provide higher-level functionality. Our
approach is based on (1) encapsulating the details of consensus into a
simple atomic primitive, (2) a decidability result for parameterized
verification of safety properties of systems with such consensus
primitives, and (3) decision procedures for parameterized synthesis. We
have used our tool to synthesize coordination for several examples of
distributed applications, including a model of the Small Aircraft
Tracking System.

Bio:
Roopsha Samanta is an Assistant Professor in the Department of Computer
Science at Purdue University. Her research mission is to make it easier
for people to build provably reliable programs. Her research focuses on
developing algorithms and tools for automated program repair and
synthesis, and targets diverse application domains such as concurrent
and distributed systems, personalized education and machine learning.

Roopsha completed her Ph.D. at The University of Texas at Austin in 2013
and was a postdoctoral researcher at the Institute of Science and
Technology Austria (IST Austria) from 2014-2016.