On Sunday, December 21th, Dr. Mohsen Lesani was the guest speaker on the topic of “Certified Concurrent and Distributed Systems”. The session held in Kharazmi Conference Hall at Computer Engineering Department, Sharif University of Technology.
You can check the abstract, and a brief bio of Dr. Lesani below.
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 proof techniques for specific classes of algorithms can simplify and automate the proof of correctness of those classes. 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.
Mohsen Lesani is an assistant professor at the Computer Science and Engineering Department of the University of California, Riverside. He spent his postdoc at MIT and obtained his PhD from UCLA. He is a BS and MS graduate from the University of Tehran and Sharif University of Technology. He has research experience with Scalable Synchronization Lab at Oracle (Sun) Labs and HP Labs. He is always looking for motivated students. The overarching goal of his research is to make computing systems more reliable and efficient. He is broadly interested in formal methods and concurrent and distributed computing. He applies program analysis and verification techniques to specify and verify concurrent and distributed systems.