Sanjit A. Seshia

  Professor
  Department of Electrical Engineering and Computer Sciences
  and Group in Logic and the Methodology of Science
  University of California, Berkeley
 
 
  Contact Information  
[   Biography   |   Publications   |   Research   |   Software   |   Teaching   |   Students & Postdocs   |   CV (in PDF)   ]
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 builds upon and extends the UCLID project, one of the first projects to develop SMT solvers and SMT-based verification methods.
  • 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 as a foundation for the synthesis of formal artifacts (e.g., programs, specifications, controllers) from examples with provable guarantees of correctness. Notable demonstrated applications to date include specification synthesis, timing analysis of embedded software, program synthesis, and controller synthesis.
  • New Application Frontiers: We pursue new applications of formal methods that illuminate foundational questions. Our current focus is in two areas: cyber-physical systems (CPS) and computer security. In CPS, we are particularly interested in 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", a concept we call control improvisation.
My group participates in the following three multi-institution projects:
  • VeHICaL: Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems
  • TSRC: TerraSwarm Research Center
  • ExCAPE: Expeditions in Computer Augmented Program Engineering
Our work on the design and verification of cyber-physical systems has led to the founding of a startup, Decyphir, Inc. We have 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.
NEW: Second edition has been published with MIT Press! Our textbook has been adopted in over 50 countries.

We recently offered a "massive open online course" (MOOC) on Cyber-Physical Systems on the edX platform: EECS149.1x. This MOOC is 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, in Spring 2014, I 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.


Note to prospective students and postdocs

   Research

Areas of Interest

Formal Methods, Dependable Computing, Computational Logic, Computer Security, Electronic Design Automation, Embedded Systems, Program Analysis, Synthetic Biology, Theory.

Publications

Full publications list, organized by

Selected Recent Talks:

Here are videos/slides from selected recent presentations:

Affiliations

Centers/Large Projects my group participates in:
  • VeHICaL: Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems
  • TSRC: TerraSwarm Research Center
  • ExCAPE: Expeditions in Computer Augmented Program Engineering
  • iCyPhy: Industrial Cyber-Physical Systems Center
  • DOP Center: Donald O. Pederson Center for Electronic Systems Design
  • CHESS: Center for Hybrid and Embedded Software Systems
Past centers:
  • GSRC: Gigascale Systems Research Center
  • SCRUB: Secure Computing Research for Users' Benefit
  • MuSyC: Multiscale Systems Center
  • TRUST: Team for Research in Ubiquitous Secure Technology
  • OSQ: Open Source Quality Project

Past Research Projects

(click on a project name for further details)
  • VGER: Verification-Guided Error Resilience of Circuits and Systems
  • Robust Embedded Systems: Verification and Learning for Provably Dependable Embedded Systems
  • SOS -- Solvers for Security: SAT, SMT, and Constraint-Based Techniques for Analyzing Security and Building Secure Systems

Descriptions of other past projects are also available.

   Software

Over the years, my group members and I have developed several software toolkits related to formal methods and its applications.
Here are some software packages that we actively develop and support:
The following software distributions are not being actively developed but are still available publicly with documentation:

   Teaching

Current

Spring 2017: On Sabbatical.

Recent Past

Fall 2016: CS 70: Discrete Mathematics and Probability Theory (co-taught with Jean Walrand)
Spring 2016: EECS 219C: Computer-Aided Verification
Fall 2015: EECS 149: Introduction to Embedded Systems
Spring 2015: EECS 219C: Computer-Aided Verification
Spring 2014: CS 294-98: Formal Methods for Engineering Education
Fall 2013:
EECS 149: Introduction to Embedded Systems (co-taught with Edward Lee)
EECS 144 & 244: Fundamental Algorithms for System Modeling, Analysis, and Optimization (co-taught with Stavros Tripakis)

Click here for the full list of courses taught.

   Group Members

Current

Ben Caulfield (Ph.D.)
Ankush Desai (Ph.D.)
Tommaso Dreossi (Postdoctoral researcher)
Daniel Fremont (Ph.D.)
Eric Kim (Ph.D.) (co-advised with Murat Arcak)
Markus Rabe (Postdoctoral researcher)
Dorsa Sadigh (Ph.D.) (co-advised with Shankar Sastry)
Yasser Shoukry (Postdoctoral researcher) (co-mentored with Paulo Tabuada and George Pappas)
Rohit Sinha (Ph.D.)
Pramod Subramanyan (Postdoctoral researcher)
Marcell Vazquez-Chanlatte (Ph.D.)

Graduated Students (with links to theses)

Wenchao Li (Ph.D.): Specification Mining: New Formalisms, Algorithms and Applications
                     (M.S.): Formal Methods for Reverse Engineering Gate-Level Netlists
Dan Holcomb (Ph.D.): Formal Verification and Synthesis for Quality-of-Service in On-Chip Networks
Susmit Jha (Ph.D.): Towards Automated System Synthesis Using Sciduction
                   (M.S.): Reachability Analysis of Lazy Linear Hybrid Automata
Bryan Brady (Ph.D.): Automatic Term-Level Abstraction
Nishant Totla (M.S.) Oracle-Guided Heap Interpolant Synthesis
Matthew Fong (M.S.): Two Optimal Path Problems in Synthetic Biology
Garvit Juniwal (M.S.): CPSGrader: Auto-Grading and Feedback Generation for Cyber-Physical Systems Education
Wei Yang Tan (M.S.): Formal Modeling and Verification of CloudProxy
Zach Wasson (M.S.): Analyzing Data-Dependent Timing and Timing Repeatability with GameTime
Jonathan Kotker (M.S.): The Internals of GameTime: Implementation and Evaluation of a Timing Analyzer for Embedded Software
Rhishikesh Limaye (M.S.): Beaver: An SMT Solver for Quantifier-free Bit-vector Logic

"Graduated" Postdocs

Alexandre Donze
Ruediger Ehlers (co-mentored with Hadas Kress-Gazit)
Daniel Bundala
Vasu Raman (co-mentored with Richard Murray)
Indranil Saha (co-mentored with George Pappas)
Yi-Chin Wu (co-mentored with Stephane Lafortune)

A complete list of current and past students, including undergraduate advisees, and postdoctoral researchers is available in my CV.

   Professional Activities

Selected Program Committees: (recent)
   CAV '16: 28th International Conference on Computer-Aided Verification
   VSTTE '15: 7th Working Conference on Verified Software: Theories, Tools, and Experiments (Program co-chair)
   FM '15: 20th International Symposium on Formal Methods
   CAV '12: 24th International Conference on Computer-Aided Verification (Program co-chair)

Other Conference/Workshop Organization: (recent)
   Dagstuhl Seminar on Machine Learning and Formal Methods, August 2017 (co-organizer)
   Dagstuhl Seminar on Decision Procedures and Abstract Interpretation, August 2014 (co-organizer)

A complete list of professional activities is available in my CV.

   Miscellaneous

Advice for students and others, compiled by Michael Ernst

My academic genealogy (courtesy the Mathematics Genealogy Project)

A partial list of "popular press" articles about research my group has contributed to: