Sanjit A. Seshia
Department of Electrical Engineering and Computer Sciences
and Group in Logic and the Methodology of Science
University of California, Berkeley
Affiliated Faculty, Industrial Cyber-Physical Systems Center, Berkeley AI Research,
and the Simons Institute for the Theory of Computing.
Contact Information
Biography: Brief, Full
A particular focus is on formal methods, which are mathematical techniques to model, design, and verify computing systems using computational proof engines. We seek to advance the state-of-the-art in automated formal methods through the following thrusts:
- Computational Engines: We develop efficient algorithms and tools for core computational problems such as satisfiability modulo theories (SMT) solving, model counting, and syntax-guided synthesis. Our focus is on identifying new classes of these problems along with novel motivating applications (such as robot motion planning). This work continues a line of research that started with UCLID, one of the first projects to develop SMT solvers and SMT-based verification methods. UCLID5 is our current active project in this thrust.
- Algorithmic Strategies for Verification and Synthesis:
We are developing new formal verification and synthesis
techniques based on a combination of inductive inference and deductive reasoning, an approach outlined with illustrative applications in
this journal paper.
We are developing a theory of
formal inductive synthesis
to provide a formal foundation for synthesis (of programs, specifications, controllers, etc.)
from examples with provable guarantees of correctness.
Notable demonstrated applications include
specification synthesis,
timing analysis of embedded software,
program synthesis, and
controller synthesis.
See this brief video for a
perspective on oracle-guided inductive synthesis
presented during the Most Influential Paper award session at ICSE 2020.
We are also developing novel techniques for achieving the goal of Verified Artificial Intelligence, implemented in open-source tools VerifAI and Scenic, which we have demonstrated for the evaluation of autonomous vehicles, both in simulation and on the road (see here for more information). - New Application Frontiers: We pursue new applications of formal methods that illuminate foundational questions. Our current focus is in the following areas: cyber-physical systems (CPS), particularly those based on artificial intelligence (AI) and machine learning (ML), and computer security across the hardware-software interface. In CPS, we are working on verification and control of Human-CPS, cyber-physical systems that operate in concert with humans, such as semi-autonomous vehicles (see sample paper). In security, we are currently focused on systems that leverage trusted hardware-software platforms (see sample paper). We are also developing theory and applications of "algorithmic improvisation", based on the core underlying problem termed as control improvisation (see this page for more details).
- VeHICaL: Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems
- LOGiCS: Learning-Based Oracle-Guided Compositional Symbiotic Design of Cyber-Physical Systems
- RDI: Center for Responsible, Decentralized Intelligence
- HICON-LEARN: Design of HIgh CONfidence LEARNing-Enabled Systems (under the DARPA Assured Autonomy program)
- BDD: Berkeley Deep Drive
Our work on the verification of automotive powertrain systems led to the founding of a startup, Decyphir, Inc. We also contributed to the ACT project at Berkeley, addressing modeling, verification, and synthesis problems in synthetic biology, resulting in the founding of 20n Labs, Inc.
I have co-developed, with Edward A. Lee, an undergraduate course on Embedded Systems
(check out the website for course material including cool videos
of student projects).
We also have an accompanying textbook
Introduction to Embedded Systems: A Cyber-Physical Systems Approach currently in its second edition published by MIT Press. Our textbook has been adopted in over 50 countries.
We offered a "massive open online course" (MOOC) on Cyber-Physical Systems on the edX platform: EECS149.1x. This MOOC was the first, to our knowledge, to employ formal verification in the automatic grading system (which was designed using inductive synthesis). More information about the automatic grading software, CPSGrader, is available here. Related to this effort, I have taught a graduate-level course on Formal Methods for Engineering Education.
Selected talks and further details on
research and teaching are available.
A good starting point is to browse my
recent publications.