Please note: This seminar will take place in DC 1304.
Federico Mora, PhD candidate
Department of Electrical Engineering and Computer Sciences
University of California, Berkeley
Distributed systems are pervasive today, from cloud computing to Internet-of-Things (IoT) systems to connected automotive vehicles. However, building dependable distributed systems remains a challenging problem. While major strides have been made in formal methods for verifying distributed systems, successful users of formal methods must be both domain experts and experts in automated reasoning — a rare combination. My work seeks to address this challenge by taking a domain-specific full-stack approach to automated reasoning that is both usable and scales to industrial systems.
In this talk, I present a new automated reasoning stack for the verification of distributed systems. This stack has three key components: the PVerifier, Algaroba, and Eudoxus. The PVerifier extends P, a programming language that developers are already using to test their distributed system designs, with support for formal verification. To do this, the PVerifier generates satisfiability modulo theories (SMT) queries that Algaroba solves. Algaroba is the fastest SMT solver in the world for the theory of quantifier-free algebraic data types (ADTs). Finally, Eudoxus is a neuro-symbolic text-to-code tool that helps automate the interaction with verification engines, like the PVerifier.
Together, these components represent the beginning of a broader vision for automated reasoning: one whose fundamental principle is that the full automated reasoning stack should be tailored to users’ needs rather than the other way around.
Bio: Federico Mora is a PhD candidate at the University of California, Berkeley, where he is advised by Sanjit A. Seshia. Federico’s research focuses on automated reasoning and formal methods for software engineering. Federico is the recipient of a Qualcomm Innovation Fellowship, the Demetri Angelakos Memorial Achievement Award, and UC Berkeley’s prestigious Outstanding Graduate Student Peer Mentor Award.