Sanjit A. Seshia

  Associate Professor
  Department of Electrical Engineering and Computer Sciences
  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. We seek to advance the state-of-the-art in automated formal methods through the following thrusts:

  • Computational Engines: We develop efficient satisfiability modulo theories (SMT) solvers and devise novel modeling and verification techniques to demonstrate new applications of these solvers. I co-lead the UCLID project, one of the first projects to develop SMT solvers and SMT-based verification methods. Current application areas include computer security, hardware design, and synthetic biology.
  • 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 we term sciduction and describe in this position paper. Demonstrated applications to date include timing analysis of embedded software, program synthesis, and controller synthesis.
  • Verification of, by, and for Human Users: In spite of advances in automation, human users remain central to the design, verification, and operation of computing systems. We are developing verification and synthesis techniques for interactive systems, such as semi-autonomous cars, where humans are central to correct operation. We are also researching novel ways of involving humans in the verification process, including crowdsourced games. Finally, we are developing new methods to infer specifications, such as our recent work based on sparse coding.
My group participates in the following three multi-institution projects:
  • TSRC: TerraSwarm Research Center
  • ExCAPE: Expeditions in Computer Augmented Program Engineering
  • SCRUB: Secure Computing Research for Users' Benefit
We have also contributed to the ACT project at Berkeley, addressing modeling, verification, and synthesis problems in synthetic biology. This work has resulted 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: We just finished offering 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. 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.


Note to prospective students and postdocs

   Research

Areas of Interest

Dependable Computing, Formal Methods, 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 my students and I participate in:
  • DOP Center: Donald O. Pederson Center for Electronic Systems Design
  • CHESS: Center for Hybrid and Embedded Software Systems
  • TSRC: TerraSwarm Research Center
  • ExCAPE: Expeditions in Computer Augmented Program Engineering
  • SCRUB: Secure Computing Research for Users' Benefit
Past centers:
  • GSRC: Gigascale Systems Research Center
  • 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

Here are some software packages that my group members and I have developed:

   Teaching

Current

Spring 2014: CS294-98: Formal Methods for Engineering Education.

Recent Past

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)
Spring 2013: On sabbatical.
Fall 2012:
EECS 219C: Computer-Aided Verification
EECS 149: Introduction to Embedded Systems (co-taught with Edward Lee)
Fall 2011: EECS 144 & 244: Fundamental Algorithms for System Modeling, Analysis, and Optimization (co-taught with Edward Lee and Jaijeet Roychowdhury)
Spring 2011:
EECS 219C: Computer-Aided Verification
EECS 149: Introduction to Embedded Systems (co-taught with Edward Lee)
Fall 2010: EECS 144 & 244: Fundamental Algorithms for System Modeling, Analysis, and Optimization (co-taught with Edward Lee and Jaijeet Roychowdhury)
Spring 2010: CS 172: Computability and Complexity

Click here for the full list of courses taught.

   Group Members

Current

Ankush Desai (Ph.D.)
Alexandre Donze (Postdoctoral researcher)
Matthew Fong (M.S.)
Daniel Fremont (Ph.D.)
Garvit Juniwal (Ph.D.)
Eric Kim (Ph.D.) (co-advised with Murat Arcak)
Vasu Raman (Postdoctoral researcher) (co-mentored with Richard Murray)
Dorsa Sadigh (Ph.D.) (co-advised with Shankar Sastry)
Indranil Saha (Postdoctoral researcher) (co-mentored with George Pappas)
Rohit Sinha (Ph.D.)
Nishant Totla (Ph.D.)

Graduated

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
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

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

   Professional Activities

Editorial Board:
   IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Program Committees: (recent)
   FM '15: 20th International Symposium on Formal Methods
   CAV '12: 24th International Conference on Computer-Aided Verification (Program co-chair)

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 contributions from my group: