Sanjit A. Seshia
Department of Electrical Engineering and Computer Sciences
University of California, Berkeley
Contact Information
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.
- TSRC: TerraSwarm Research Center
- ExCAPE: Expeditions in Computer Augmented Program Engineering
- SCRUB: Secure Computing Research for Users' Benefit
We also have an accompanying textbook Introduction to Embedded Systems: A Cyber-Physical Systems Approach.
Selected talks and further details on
research and teaching are available.