Prof. Seshia's 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) and SMT-based verification, through the UCLID system, one of the first SMT solvers and SMT-based verifiers, and its successor, UCLID5. He has also led work on formal (provably-correct) inductive synthesis of programs, specifications, and controllers, showing how algorithmic synthesis and learning is central to the field of formal methods. His group has also made foundational and wide-ranging contributions to formal methods for CPS and AI systems, including simulation-based verification and formal synthesis of CPS, learning logical specifications from data and demonstrations, and theory and tools for verified AI-based autonomy. He has co-authored over 200 refereed publications in journals and conferences in his areas of expertise, and several of these have received best paper awards. His work has been widely adopted in industry, with technology deployments by both large companies and startups, spanning domains such as chip design, cloud computing, automotive powertrain systems, and autonomous vehicles. He has served as Lead PI of large, multi-year, multi-university projects, including the National Science Foundation (NSF) CPS Frontier project, VeHICaL, and the DARPA Symbiotic Design of CPS project LOGiCS.
Prof. Seshia has also made numerous contributions to higher education and mentoring. He co-created a new undergraduate course on embedded, cyber-physical systems at UC Berkeley, EECS 149, and is co-author of a widely-used textbook on this topic, Introduction to Embedded Systems: A Cyber-Physical Systems Approach, published by MIT Press (now in second edition). He has also led the development of technologies for cyber-physical systems education based on formal methods. His team created the CPSGrader system for CPS virtual laboratories with automated grading and feedback, deployed successfully in one of the very first massive open online courses on CPS, EECS 149.1x on edX, and during the COVID-19 pandemic. He has given numerous invited talks and tutorials. He has advised over 40 graduate students and over 20 postdoctoral researchers, as well as numerous undergraduate student researchers.
Prof. Seshia also has an extensive track record of service to the profession and his university. He served as a Program Chair for the 2012 International Conference on Computer-Aided Verification (CAV) and the 2020 ACM International Conference on Hybrid Systems: Computation and Control. He has served as Associate Editor for several journals including the IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems and the ACM Transactions on Embedded Computing Systems. Prof. Seshia's service to UC Berkeley includes four years as a Chair for Graduate Admissions in the EECS Department at UC Berkeley, and several years on the campus-level committee on Undergraduate Scholarships, Honors, and Financial Aid. Additionally, he has served on several national and international advisory committees including the Scientific Committee of the Gran Sasso Science Institute, Italy, and the Steering Committee and Technical Working Group of the World Economic Forum (WEF) Safe Drive Initiative.
Prof. Seshia's awards and honors include a U.S. 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 ACM/IEEE International Conference on Software Engineering Most-Influential Paper Award (for 2010-20), the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award for fundamental contributions to formal methods for CPS design and to CPS education, and the Computer-Aided Verification (CAV) Award for pioneering contributions to the foundations of SMT solving. He is a Fellow of both the Association for Computing Machinery (ACM) and the Institute of Electrical and Electronics Engineers (IEEE).