Speaker: Elaine Li (New York University)
Title: Abstractions for Building Verified Distributed Systems
The seminar will be available for in-person and Zoom participation. To participate online, please email inquiry-cs@barnard.edu to receive the Zoom link.
Distributed systems are ubiquitous, safety-critical, yet error-prone, making them a prime target for formal verification. Formal verification is the use of mathematical reasoning to rigorously guarantee the absence of software bugs. In my talk, I will showcase how automata theory can be fruitfully applied to distributed systems verification problems. I will first focus on the abstraction of global protocols, which serve as a blueprint for synthesizing correct-by-construction implementations. I explain how an automata-theoretic lens enabled the design of a protocol verification tool that improves on prior work in terms of completeness and expressivity, without sacrificing efficiency. Next, I will propose compositional verification methods that mirror the incremental nature of systems development, again drawing inspiration from automata theory. I will conclude with a discussion of future work on developing verification tools and abstractions with AI users in mind.
Elaine Li is a Faculty Fellow at the Courant Institute of New York University. Her research interests are in logic, automata theory, and formal verification. She obtained her PhD in Computer Science from NYU in 2025, and her Bachelor of Science from Yale-NUS College in 2019.