Sanjit Seshia's Home

	Sanjit A. Seshia
	Assistant Professor Department of Electrical Engineering and Computer Sciences University of California, Berkeley Contact Information
[ Biography \| Publications \| Research \| Software \| Teaching \| CV (in PDF) ]
What's NEW: Research: Satisfiability Modulo Theories (book chapter) Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits Optimizations of an Application-Level Protocol for Enhanced Dependability in FlexRay Teaching: EECS 149: Introduction to Embedded Systems Events/Journals: (please submit your best papers!) QA'09: Workshop on Quantitative Analysis of Software (co-located with CAV '09) IEEE Embedded Systems Letters Note to prospective students

Research

My research develops algorithmic techniques for dependable and secure computing. Problems of interest range over several abstraction layers, from algorithms, through software, to circuits.

Areas of Interest

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

Current Research Projects

(click on a project name for further details)

UCLID: Reasoning about Computer Systems using Boolean Methods
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 System Security

I also collaborate with Rastislav Bodik on the Sketching project.

Descriptions of past projects are also available.

Publications

Here are some recent publications:

See the publications page for further details about my current and past research.

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
GSRC: Gigascale Systems Research Center
OSQ: Open Source Quality Project
TRUST: Team for Research in Ubiquitous Secure Technology

Software

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

UCLID: A system for modeling and verifying hardware, software, and protocols in a subset of first-order logic with efficient SAT-based decision procedures
Beaver: A satisfiability-modulo-theories (SMT) solver for finite-precision bit-vector arithmetic
v2ucl: An abstraction tool for generating UCLID models from Verilog descriptions of hardware
BFIT: The Berkeley FIT (failure-in-time) Estimation Tool

Teaching

Current

Spring 2009:
EECS 149: Introduction to Embedded Systems

Past

Fall 2008: EECS 244: Introduction to Computer-Aided Design of ICs (co-taught with Kurt Keutzer)
Spring 2008:
CS 172: Computability and Complexity
EECS 124: Introduction to Embedded Systems (co-taught with Edward Lee)
Fall 2007:
EECS 244: Introduction to Computer-Aided Design of ICs (co-taught with Kurt Keutzer)
CS 294-25: Current Berkeley Research in Programming Systems (co-taught with R. Bodik, K. Sen, D. Song, and K. Yelick)
Spring 2007: EECS 219C: Computer-Aided Verification
Fall 2006: CS 172: Computability and Complexity
Spring 2006: EECS 219C: Computer-Aided Verification
Fall 2005: EECS 244: Introduction to Computer-Aided Design of ICs (co-taught with Kurt Keutzer)

Students

Graduate

Bryan Brady
Dan Holcomb
Susmit Jha
Wenchao Li
Rhishikesh Limaye

Undergraduate

Miscellaneous

Advice for students and others, compiled by Michael Ernst

My academic genealogy (courtesy the Mathematics Genealogy Project)

An article about some of my research.