IEEE CEDA Distinguished Speaker at ESWEEK 2025: Sanjit A. Seshia

The IEEE Council on Electronic Design Automation is pleased to host the CEDA Distinguished Speaker Luncheon at ESWEEK 2025. The event will be held on Tuesday, 30 September 2025. This year’s distinguished speaker is Sanjit A. Seshia, Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. Professor Seshia will share insights on how formal methods and artificial intelligence have evolved and where they are headed, with perspectives spanning past breakthroughs, present applications, and future possibilities. Join colleagues and experts for this special luncheon session and gain valuable perspectives from one of the leading voices in the field. 

Talk Title: Full-Stack AI-Enabled Formal Methods: Past, Present, and Future

Abstract: 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 desig