Sanjit A. Seshia

Associate Professor

Research Areas

• Design, Modeling and Analysis (DMA)
• Programming Systems (PS)
• Security (SEC)
• Dependable Computing; Computational Logic; Formal Methods

Research Centers

• Center for Hybrid and Embedded Software Systems (CHESS)
• Donald O. Pederson Center for Electronics Systems Design (DOP)
• Gigascale Systems Research Center (GSRC)
• Multiscale System Center (MuSyC)
• Secure Computing Research for Users' Benefit (SCRUB)
• Team for Research in Ubiquitous Secure Technology (TRUST)
• TerraSwarm Research Center

Teaching Schedule (Fall 2013)

• CS C149. Introduction to Embedded Systems, TuTh 11-1230P, 306 Soda
• CS C249A. Introduction to Embedded Systems, TT 11:00-12:30P, 306 Soda
• EE 144. Fundamental Algorithms for Systems Modeling, Analysis, and Optimization, TuTh 330-5P, F10-11A, 540A/B Cory
• EE C149. Introduction to Embedded Systems, TuTh 11-1230P, 306 Soda
• EE 244. Fundamental Algorithms for Systems Modeling, Analysis, and Optimization, TT 3:30-5:00P, 540A/B Cory
• EE C249A. Introduction to Embedded Systems, TT 11:00-12:30P, 306 Soda

Biography

He received his B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay and a M.S. and a Ph.D. in Computer Science from Carnegie Mellon University. His Ph.D. thesis research on the UCLID verification system pioneered the area known as satisfiability modulo theories (SMT) and SMT-based verification. He has co-authored a textbook on embedded systems. He has received a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.

Selected Publications

• O. Kupferman, W. Li, and S. A. Seshia, "A theory of mutations with applications to vacuity, coverage, and fault tolerance," in Proc. 2008 Formal Methods in Computer Aided Design Conf. (FMCAD '08), A. Cimatti and R. Jones, Eds., Los Alamitos, CA: IEEE Computer Society, 2008, pp. 9 pg.
• S. A. Seshia, "Autonomic reactive systems via online learning," in Proc. 4th Intl. Conf. on Autonomic Computing (ICAC 2007), Piscataway, NJ: IEEE Press, 2007, pp. 162-171.
• A. Solar Lezama, G. Arnold, L. Tancau, R. Bodik, V. Saraswat, and S. A. Seshia, "Sketching stencils," in Proc. 2007 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI '07), New York, NY: The Association for Computing Machinery, Inc., 2007, pp. 167-178.
• S. A. Seshia, W. Li, and S. Mitra, "Verification-guided soft error resilience," in Proc.10th Design, Automation and Test in Europe Conference and Exhibition (DATE '07), San Jose, CA: EDA Consortium, 2007, pp. 1442-1447.
• S. A. Seshia and R. E. Bryant, "Deciding quantifier-free Presburger formulas using parameterized solution bounds," Logical Methods in Computer Science, vol. 1, no. 2, pp. 1-26, Dec. 2005.
• V. Ganapathy, S. A. Seshia, S. Jha, T. W. Reps, and R. E. Bryant, "Automatic discovery of API-level exploits," in Proc. 27th Intl. Conf. on Software Engineering (ICSE '05), New York, NY: ACM Press, 2005, pp. 312-321.
• S. A. Seshia, R. E. Bryant, and K. S. Stevens, "Modeling and verifying circuits using generalized relative timing," in Proc. 11th IEEE Intl. Symp. on Asynchronous Circuits and Systems (ASYNC 2005), Los Alamitos, CA: IEEE Computer Society, 2005, pp. 98-108.
• S. A. Seshia, S. K. Lahiri, and R. E. Bryant, "A hybrid SAT-based decision procedure for separation logic with uninterpreted functions," in Proc. 40th IEEE/ACM Design Automation Conf. (DAC 2003), New York, NY: The Association for Computing Machinery, Inc., 2003, pp. 425-430.
• R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions," in Computer Aided Verification: Proc. 14th Intl. Conf. (CAV 2002), E. Brinksma and K. Guldstrand Larsen, Eds., Lecture Notes in Computer Science, Vol. 2404, Berlin, Germany: Springer-Verlag, 2002, pp. 79-82.