Sanjit A. Seshia

Our work focuses in particular on formal methods, which are mathematical techniques to model, design, and analyze computer systems. We seek to advance the state-of-the-art in formal methods at multiple levels, including:

• Computational Engines: We develop efficient satisfiability modulo theories (SMT) solvers and devise novel modeling techniques to demonstrate new applications of these solvers. See the UCLID project for more details.
• 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. See this technical report for further details.
• Design for Verification and Resilience: System correctness and reliability is best ensured when the system is designed with those criteria in mind. We are therefore researching techniques to better integrate design, specification, and verification to facilitate the development of robust, error-resilient systems, at low resource overheads.

Areas of Interest

Current Research Projects

• 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 Security and Building Secure Systems

Descriptions of past projects are also available.

Publications

• Type
• Area
• Year

• Abstraction-Based Performance Analysis of NoCs - (DAC 2011)
• Counterexample-Guided SMT-Driven Optimal Buffer Sizing - (DATE 2011)
• ATLAS: Automatic Term-Level Abstraction of RTL Designs - (MEMOCODE 2010)
• Scalable Specification Mining For Verification and Diagnosis - (DAC 2010)
• Post-Silicon Validation: Opportunities, Challenges and Recent Advances - (DAC 2010)
• Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits - (DATE 2009)
• Verification-Guided Soft Error Resilience - (DATE 2007)

• Timing Analysis of Interrupt-Driven Programs under Context Bounds - (FMCAD 2011)
• Synthesis of Optimal Switching Logic for Hybrid Systems - (EMSOFT 2011)
• Distributed Real-Time Software for Cyber-Physical Systems - (Proc. IEEE 2011)
• Quantitative Analysis of Software: Challenges and Recent Advances - (Invited paper)
• Quantitative Analysis of Systems Using Game-Theoretic Learning - (ACM TECS)
• GameTime: A Toolkit for Timing Analysis of Software - (TACAS 2011)
• Synthesizing Switching Logic for Safety and Dwell-Time Requirements - (ICCPS 2010)
• Game-Theoretic Timing Analysis - (ICCAD 2008)
• The Case for Timing-Centric Distributed Software - (WCPS 2009)

• Oracle-Guided Component-Based Program Synthesis - (ICSE 2010)
• Automating Security Mediation Placement - (ESOP 2010)
• On Voting Machine Design for Verification and Testability - (CCS 2009)

• Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis - (TR 2011)
• Satisfiability Modulo Theories - (chapter in Handbook of Satisfiability, IOS Press)
• Synthesis with Clairvoyance - (HVC 2011)
• Learning Conditional Abstractions - (FMCAD 2011)
• Mining Assumptions for Synthesis - (MEMOCODE 2011)
• CalCS: SMT Solving for Non-Linear Convex Constraints - (FMCAD 2010)
• Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic - (CAV 2009)
• Autonomic Reactive Systems via Online Learning - (ICAC 2007)
• Deciding Bit-Vector Arithmetic with Abstraction - (TACAS 2007).

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

Recent Courses

Click here for the full list of courses taught.

Current

Graduated

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

Program Committees: (recent)
   CAV '12: 24th International Conference on Computer-Aided Verification (Program co-chair)
   SMT '11: International Workshop on Satisfiability Modulo Theories (Program co-chair)
   ICCAD'11: International Conference on Computer-Aided Design (chair of Verification track)
   CAV '11: 23rd International Conference on Computer-Aided Verification
   NFM '11: 3rd NASA Formal Methods Symposium
   EMSOFT'10: International Conference on Embedded Software

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

Advice for students and others, compiled by Michael Ernst

My academic genealogy (courtesy the Mathematics Genealogy Project)

An article about some of my research.