Sanjit A. Seshia
Department of Electrical Engineering and Computer Sciences
and Group in Logic and the Methodology of Science
University of California, Berkeley
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:
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 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.
Areas of InterestFormal Methods, Dependable Computing, Computational Logic, Computer Security, Electronic Design Automation, Embedded Systems, Program Analysis, Synthetic Biology, Theory.
PublicationsFull publications list, organized by
Selected Recent Talks:Here are videos/slides from selected recent presentations:
AffiliationsCenters/Large Projects my group participates in:
Past Research Projects(click on a project name for further details)
Descriptions of other past projects are also available.
CurrentSpring 2018: EECS 219C: Formal Methods: Specification, Verification, and Synthesis
Recent PastSpring & Fall 2017: On Sabbatical.
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
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.
CurrentBen Caulfield (Ph.D.)
Ankush Desai (Ph.D.)
Tommaso Dreossi (Postdoctoral researcher)
Daniel Fremont (Ph.D.)
Shromona Ghosh (Ph.D.) (co-advised with Alberto Sangiovanni-Vincentelli)
Mark Ho (Postdoctoral researcher) (co-mentored with Tom Griffiths on the VeHICaL project)
Edward Kim (Ph.D.) (co-advised with Alberto Sangiovanni-Vincentelli)
Eric Kim (Ph.D.) (co-advised with Murat Arcak)
Markus Rabe (Postdoctoral researcher)
Pramod Subramanyan (Postdoctoral researcher)
Marcell Vazquez-Chanlatte (Ph.D.)
Graduated Students (with links to theses)Rohit Sinha (Ph.D.): Secure Computing using Certified Software and Trusted Hardware
Dorsa Sadigh (Ph.D.) (co-advised with Shankar Sastry): Safe and Interactive Autonomy: Control, Learning, and Verification
Rafael Valle (Ph.D.) (co-advised with Edmund Campion): Data Hallucination, Falsification and Validation using Generative Models and Formal Methods
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 (reverse chronological order)Yasser Shoukry (co-mentored with Paulo Tabuada and George Pappas)
Yi-Chin Wu (co-mentored with Stephane Lafortune)
Vasu Raman (co-mentored with Richard Murray)
Indranil Saha (co-mentored with George Pappas)
Ruediger Ehlers (co-mentored with Hadas Kress-Gazit)
A complete list of current and past students, including undergraduate advisees, and postdoctoral researchers is available in my CV.
Selected Program Committees: (recent)
Other Conference/Workshop Organization: (recent)
A complete list of professional activities is available in my CV.
A partial list of "popular press" articles about research my group has contributed to: