Sanjit Seshia's Home (original) (raw)
My research group develops _theory and tools_to aid the construction of provably dependable and secure systems. Our work spans several abstraction layers, from mathematical models, through software, to electronic and biological substrates.
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 synthesisto provide a formal foundation for synthesis (of programs, specifications, controllers, etc.) from examples with provable guarantees of correctness. Notable demonstrated applications includespecification 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 toolsVerifAI 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 ofHuman-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 ascontrol improvisation (see this page for more details). My group participates in the following large projects:
- 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 We are also part of iCyPhy, the Industrial Cyber-Physical Systems Center, and BAIR, Berkeley AI Research. I am also affiliated with the Simons Institute for the Theory of Computing.
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.