Speaker: Mohsen Lesani
Location: Soda Hall, 510
Date: Friday, Feb 20th, 2026
Time: 12-1 pm PT
Title: Generation of Verified Distributed Systems
Abstract:
Distributed systems are the backbone of modern computing. Yet, building distributed systems with reliability and security guarantees has proven to be complicated, and remains elusive. This complication is not only faced by experts that design and implement distributed systems but is also exposed to client programmers that develop distributed applications. This talk presents an overview of our cross-stack research on automatic generation of coordination for applications, and mechanized verification for distributed middleware. I then present a project that, given a sequential class with the declaration of its integrity and recency requirements, automatically generates a correct-by-construction replicated class that guarantees integrity, convergence and recency, and avoids coordination when possible. The approach is based on a novel sufficient condition called well-coordination for integrity and convergence which requires certain orders between conflicting and dependent operations. Our generation tools apply automatic solvers to statically derive the conflict and dependency relations. They then reduce the coordination avoidance problem to classical graph minimization problems, and use the results to instantiate parametric coordination protocols, and generate replicated stores. We applied this approach to message-passing networks and then extended it to RDMA and FPGA accelerated networks, and further applied a variant to coordinate actions on augmented reality objects.
Speaker Bio:
Mohsen Lesani is an associate professor at the Computer Science and Engineering department of the University of California, Santa Cruz. He is spending his sabbatical at UCB. He spent his postdoc at MIT and obtained his PhD from UCLA. His research interests are formal methods and distributed systems. He received the NSF CAREER award in 2020 and the DARPA YFA in 2022. His research has been recognized as SIGPLAN Research Highlight and received the distinguished paper award at OOPSLA.