Talk Title: Unbounded Protocols: Building Blocks of Scalable and Fault-tolerant Distributed Systems
Abstract: Modern distributed systems (e.g., peer-to-peer systems, distributed key-value storage, distributed AI) are very complex because they must be scalable, fault-tolerant, and self-organizing in the absence of a central coordinator. The simultaneous possession of multiple properties makes the design and verification of such systems a daunting task, evidenced by protocols whose proof of correctness takes years (e.g., Chord for distributed hashing). Another complicating factor includes the unboundedness of such systems as they are required to function correctly for an unbounded number of nodes. Thus, it is highly desirable to provide tools that automate the design and verification of distributed systems for mainstream engineers.
This talk includes two parts. First, I will provide a brief overview of some of our past/ongoing projects related to design and implementation of highly dependable software such as Automated Air Traffic Management, Cyber Physical Systems, IoT networks, and synthesis of computationally-efficient neural networks for resource-constrained systems. Then, I will present our most recent research on automated synthesis and verification of unbounded distributed protocols that preserve their correctness, resilience and self-organizing properties regardless of their scale.