|
Computer Science Seminar Date: Friday, 18 July 2025 Time: 11:30 AM Venue: Lecture Hall 202 Full-Stack Automated Reasoning with UCLID5 Sanjit A Seshia University of California, Berkeley. 18-07-25 Abstract Formal methods are crucial for ensuring the dependability and security of our computing infrastructure, spanning software, hardware, and distributed and networked systems. In order to be scalable and usable, these formal methods require a full-stack approach to automated reasoning, where the computational hardness of the underlying reasoning problems is mitigated by domain-specific modeling and reasoning strategies. In this talk, I will present a full-stack automated reasoning approach pioneered by the UCLID5 formal modeling and verification system. UCLID5 embraces a multi-modal approach to formal methods which fits well with the needs to model heterogeneous systems including combinations of hardware and software, real-time embedded systems, and complex distributed systems. I will describe the motivation and overall architecture of UCLID5, as well as its applications to verifying distributed systems used in industrial cloud computing. The talk will cover novel contributions to SMT solving, formal verification and synthesis strategies, as well as techniques to ease the process of creating UCLID5 models using large language models. Specific contributions covered in this talk include the PVerifier, Algaroba, and Eudoxus. The PVerifier extends P, a programming language already used in industry (e.g. AWS) for modeling and testing distributed systems, with support for formal verification. To do this, the PVerifier generates satisfiability modulo theories (SMT) queries solved by Algaroba, the leading SMT solver 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 UCLID5. Speaker Bio : Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, spanning the areas of cyber-physical systems (CPS), computer security, distributed systems, artificial intelligence (AI), machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award, the Computer-Aided Verification (CAV) Award for pioneering contributions to the foundations of SMT solving, and the Distinguished Alumnus Award from IIT Bombay. He is a Fellow of the ACM and the IEEE.
|
