Colloquium Details
Certified Concurrent and Distributed Systems
Speaker: Mohsen Lesani, MIT
Location: Warren Weaver Hall 1302
Date: February 12, 2016, 11:30 a.m.
Host: Subhash Khot
Synopsis:
Aspects of concurrency and distribution pervasively appear in modern computing systems, including personal devices, data centers, aircrafts and medical devices. Due to complicated interactions between processes, concurrent and distributed systems are subtle and prone to bugs. Such bugs have led to death of patients and blackouts with millions of dollars financial loss. Can we build concurrent and distributed systems with static safety and security guarantees?
In this talk, I present how we can exploit advances in formal methods to develop correct-by-construction concurrent and distributed systems. In particular, I show how modern SMT solvers and proof assistants can aid the development of correct concurrent data-structures and distributed data-stores. First, I introduce a proof technique called condensability and a tool called Snowflake to verify linearizability of composing concurrent data-structures in Java. Snowflake generates proof obligations for condensability and discharges them using the Z3 SMT solver. Snowflake successfully verified a large fraction of composing methods in several open-source applications. Second, I present a framework in Coq called Chapar for development and modular verification of causally consistent replicated key-value store implementations and their clients. Chapar includes a novel proof technique for causal consistency of key-value store implementations that was used to verify two key-value store implementations from the literature. Extraction from Coq to OCaml resulted in two executable stores with the static causal consistency guarantee. Finally, I describe my future plans to build certified byzantine fault-tolerant replicated stores.
Speaker Bio:
Mohsen Lesani is a postdoctoral associate at MIT CSAIL working at the intersection of formal methods and concurrent and distributed computing. Mohsen's current research focuses on building certified concurrent and distributed systems using the coq programming language and proof assistant under the advisement of Adam Chlipala. His recent work is a framework for verification of causally consistent distributed key-value stores. He obtained his PhD on testing and verification techniques for transactional memory and concurrent data-structures in 2014 from UCLA where he was advised by Jens Palsberg and worked with Todd Millstein. He received the outstanding research award from UCLA computer science department in 2014. He has research experience with Scalable Synchronization Lab at Oracle (Sun) Labs and HP Labs.
Notes:
In-person attendance only available to those with active NYU ID cards.