Roopsha Samanta
Discover[i]: Component-based Parameterized Reasoning for Distributed Applications
November 27, 2018 at 12:00pm (lunch talk) CSE 305
Abstract
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.