CEDA Tuesday Lunch Keynote
Full-Stack AI-Enabled Formal Methods: Past, Present, and Future
Formal methods are crucial for ensuring the dependability and security of our computing infrastructure, spanning software, hardware, networked, and cyber-physical systems. In order to be scalable and usable, these formal methods require a full-stack approach to automated reasoning where strategies for formal modeling, specification, verification, and synthesis are well integrated, and the computational hardness of the underlying reasoning problems is mitigated by domain-specific modeling and reasoning strategies.
In this talk, I will describe our approach to full-stack formal methods by infusing machine learning (ML) and data-driven artificial intelligence (AI) into traditional deductive automated reasoning. This approach to AI-enabled formal methods, developed over 20+ years, has been pioneered in the UCLID (pronounced “Euclid”) and UCLID5 projects. It has been demonstrated for modeling and verifying heterogeneous systems including combinations of hardware and software, real-time embedded systems, and complex distributed systems, with industrial deployments. UCLID5 embraces a multi-modal approach to formal methods which fits well with the need to model and verify heterogeneous systems. I will discuss how ML and AI can be effective across the formal methods stack, including in computational engines such as satisfiability solvers (SAT/SMT/QBF), for model checking and compositional program verification, as well as for creating formal UCLID5 models from natural language. The talk will cover foundational principles including “verification by reduction to synthesis” and oracle-guided learning, and how these subsume the use with formal methods of newer AI technologies such as large language models (LLMs). I will illustrate the key ideas with representative use cases of UCLID5, and will conclude with an outlook to the future of AI-enabled formal methods for system design.
Biography
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.
