Faculty Publications - Sanjit A. Seshia

Books

• E. A. Lee and S. A. Seshia, Introduction to Embedded Systems - A Cyber-Physical Systems Approach, Berkeley, CA: LeeSeshia.org, 2011. [abstract]

Book chapters or sections

• S. Jha, B. A. Brady, and S. A. Seshia, "Symbolic reachability analysis of lazy linear hybrid automata," in Formal Modeling and Analysis of Time Systems: Proc. 5th Intl. Conf. (FORMATS 2007), J. F. Raskin and P. S. Thiagarajan, Eds., Lecture Notes in Computer Science, Vol. 4763, Berlin, Germany: Springer-Verlag, 2007, pp. 241-256.
• R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, "Deciding bit-vector arithmetic with abstraction," in Tools and Algorithms for the Construction and Analysis of Systems: Proc. 13th Intl. Conf. (TACAS 2007), O. Grumberg and M. Huth, Eds., Lecture Notes in Computer Science, Vol. 4425, Berlin, Germany: Springer-Verlag, 2007, pp. 358-372.
• D. Kroening, J. Ouaknine, S. A. Seshia, and O. Strichman, "Abstraction-based satisfiability solving of Presburger arithmetic," in Computer Aided Verification: Proc. 16th Intl. Conf. (CAV 2004), R. Alur and D. A. Peled, Eds., Lecture Notes in Computer Science, Vol. 3114, Berlin, Germany: Springer-Verlag, 2004, pp. 308-320.
• S. K. Lahiri and S. A. Seshia, "The UCLID decision procedure," in Computer Aided Verification: Proc. 16th Intl. Conf. (CAV 2004), R. Alur and D. A. Peled, Eds., Lecture Notes in Computer Science, Vol. 3114, Berlin, Germany: Springer-Verlag, 2004, pp. 475-478.
• R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Convergence testing in term-level bounded model checking," in Correct Hardware Design and Verification Methods: Proc. 12th IFIP WG 10.5 Advanced Research Working Group (CHARME 2003), D. Geist and E. Tronci, Eds., Lecture Notes in Computer Science, Vol. 2860, Berlin, Germany: Springer-Verlag, 2003, pp. 348-362.
• S. A. Seshia and R. E. Bryant, "Unbounded, fully symbolic model checking of timed automata using Boolean methods," in Computer Aided Verification: Proc. 15th Intl. Conf. (CAV 2003), W. A. Hunt Jr. and F. Somenzi, Eds., Lecture Notes in Computer Science, Vol. 2725, Berlin, Germany: Springer-Verlag, 2003.
• S. K. Lahiri, S. A. Seshia, and R. E. Bryant, "Modeling and verification of out-of-order microprocessors in UCLID," in Formal Meethods in Computer-Aided Design: Proc. 4th Intl. Conf. (FMCAD 2002), M. D. Aagaard and J. W. O'Leary, Eds., Lecture Notes in Computer Science, Vol. 2517, Berlin, Germany: Springer-Verlag, 2002, pp. 142-159.
• 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.
• C. Flanagan, S. Qadeer, and S. A. Seshia, "A modular checker for multithreaded programs," 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. 65-78.
• O. Strichman, S. A. Seshia, and R. E. Bryant, "Deciding separation formulas with SAT," in Computer Aided Verification: Proc. 14th Intl. Conf. (CAV 2002), E. Brinksma and K. Guldstrand Larsen, Eds., Lecture Notes in Computer Science, Vol. 3835, Berlin, Germany: Springer-Verlag, 2002, pp. 113-124.
• A. K. Bhattacharjee, S. D. Dhodapkar, S. A. Seshia, and R. K. Shyamasundar, "A graphical environment for the specification and verification of reactive systems," in Computer Safety, Reliability and Security: Proc. 18th Intl. Conf. (SAFECOMP '99), M. Felici, K. Kanoun, and A. Pasquini, Eds., Lecture Notes in Computer Science, Vol. 1698, Berlin, Germany: Springer-Verlag, 1999, pp. 431-444.
• S. A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, and S. D. Dhodapkar, "A translation of Statecharts to ESTEREL," in FM '99 -- Formal Methods: Proc. World Congress on Formal Methods in the Development of Computing Systems, Vol. II, J. Wing, J. Woodcock, and J. Davies, Eds., Lecture Notes in Computer Science, Vol. 1709, Berlin, Germany: Springer-Verlag, 1999, pp. 983-1007.

Articles in journals or magazines

• J. Eidson, E. A. Lee, S. Matic, S. A. Seshia, and J. Zou, "Distributed Real-Time Software for Cyber-Physical Systems," Proceedings of the IEEE (special issue on CPS), vol. 100, no. 1, pp. 45 - 59, Jan. 2012. [abstract]
• A. Solar Lezama, G. Arnold, L. Tancau, R. Bodik, V. Saraswat, and S. A. Seshia, "Sketching stencils," ACM SIGPLAN Notices, vol. 42, no. 6, pp. 167-178, June 2007.
• S. A. Seshia, K. Subramani, and R. E. Bryang, "On solving Boolean combinations of UTVPI constraints," J. Satisfiability, Boolean Modeling and Computation: Special Issue on Satisfiability Modulo Theories, vol. 3, pp. 67-90, May 2007.
• A. Solar Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. A. Seshia, "Combinatorial sketching for finite programs," ACM SIGPLAN Notices, vol. 41, no. 11, pp. 404-415, Nov. 2006.
• 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.
• C. Flanagan, S. N. Freund, S. Qadeer, and S. A. Seshia, "Modular verification of multithreaded programs," Theoretical Computer Science, vol. 338, no. 1-3, pp. 153-183, June 2005.
• A. K. Bhattacharjee, S. D. Dhodapkar, S. A. Seshia, and R. K. Shyamasundar, "PERTS: An environment for the specification and verification of reactive systems--Corrigendum," Reliability Engineering & System Safety, vol. 72, no. 2, pp. 223, May 2001.
• A. K. Bhattacharjee, S. D. Dhodapkar, S. A. Seshia, and R. K. Shyamasundar, "PERTS: An environment for the specification and verification of reactive systems," Reliability Engineering & System Safety, vol. 71, no. 3, pp. 299-310, March 2001.

Articles in conference proceedings

• P. Nuzzo, A. A. A. Puggelli, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, "CalCS: SMT Solving for Non-linear Convex Constraints," in Formal Methods in Computer Aided Design, FMCAD 2010, 2010, pp. 71-79.
• P. Nuzzo, A. Puggelli, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, "{CalCS}: {SMT} Solving for Non-linear Convex Constraints," in Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2010, pp. 71--79.
• D. King, T. Jaeger, S. Jha, and S. A. Seshia, "Effective blame for information-flow violations," in Proc. 16th ACM SIGSOFT Intl. Symp. on the Foundations of Software Engineering (SIGSOFT 2008/FSE 16), New York, NY: The Association for Computing Machinery, Inc., 2008.
• S. A. Seshia and A. Rakhlin, "Game-theoretic timing analysis," in Proc. IEEE/ACM 2008 Intl. Conf. on Computer-Aided Design (ICCAD '08), Piscataway, NJ: IEEE Press, 2008.
• 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.
• D. Kroening and S. A. Seshia, "Formal verification at higher levels of abstraction (Tutorial)," in 2007 IEEE/ACM Intl. Conf. on Computer-Aided Design (ICCAD '07) Digest of Technical Papers, Piscataway, NJ: IEEE Press, 2007, pp. 572-578.
• D. Beyer, T. A. Henzinger, A. Chakrabarti, and S. A. Seshia, "An application of Web-service interfaces," in Proc. 2007 IEEE Intl. Conf. on Web Services (ICWS '07), Los Alamitos, CA: IEEE Computer Society, 2007, pp. 831-838.
• 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.
• T. H. Feng, L. Wang, W. Zheng, S. Kanajan, and S. A. Seshia, "Automatic model generation for black box real-time systems," in Proc. 10th Design, Automation and Test in Europe Conference and Exhibition (DATE '07), San Jose, CA: EDA Consortium, 2007, pp. 930-935.
• 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.
• A. Solar Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. A. Seshia, "Combinatorial sketching for finite programs," in Proc. 12th Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XII), New York, NY: The Association for Computing Machinery, Inc., 2006, pp. 404-415.
• M. Christodorescu, S. Jha, S. A. Seshia, D. Song, and R. E. Bryant, "Semantics-aware malware detection," in Proc. 2005 IEEE Symp. on Security and Privacy (S&P '05), Los Alamitos, CA: IEEE Computer Society, 2005, pp. 32-46.
• 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 and R. E. Bryant, "Deciding quantifier-free Presburger formulas using parameterized solution bounds," in Proc. 19th Annual IEEE Logic in Computer Science (LICS 2004), Los Alamitos, CA: IEEE Computer Society, 2004, pp. 100-109.
• 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, "Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings," in Proc. 1st Intl. Workshop on Constraints in Formal Verification (CFV 2002), 2002, pp. 18 pg.
• S. Arunkumar and S. A. Seshia, "A framework for the management of informatics and technology for enterprise excellence," in Proc. Portland Intl. Conf. on Management of Engineering Technology (PICMET '907, D. F. Kocaoglu and T. R. Anderson, Eds., Piscataway, NJ: IEEE Press, 1997, pp. 735-735.

Technical Reports

• W. Li, D. Sadigh, S. S. Sastry, and S. A. Seshia, "Synthesis for Human-in-the-Loop Control Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2013-134, July 2013. [abstract]
• A. A. A. Puggelli, W. Li, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, "Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2013-24, April 2013. [abstract]
• S. Jha and S. A. Seshia, "SWATI: Synthesizing Word-Lengths Automatically Using Testing and Induction," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2013-7, Feb. 2013. [abstract]
• E. A. Lee, J. D. Kubiatowicz, J. M. Rabaey, A. L. Sangiovanni-Vincentelli, S. A. Seshia, J. Wawrzynek, D. Blaauw, P. Dutta, K. Fu, C. Guestrin, R. Jafari, D. Jones, V. Kumar, R. Murray, G. Pappas, A. Rowe, C. M. Sechen, T. S. Rosing, B. Taskar, and D. Wessel, "The TerraSwarm Research Center (TSRC) (A White Paper)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2012-207, Nov. 2012. [abstract]
• W. Li, S. A. Seshia, and S. Jha, "CrowdMine: Towards Crowdsourced Human-Assisted Verification," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2012-121, May 2012. [abstract]
• W. Li and S. A. Seshia, "A Sparse Coding Method for Specification Mining and Error Localization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-163, Dec. 2011. [abstract]
• W. Li, S. K. Jha, and S. A. Seshia, "Power-Aware Dynamic Control of Error-Resilience Mechanisms," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-109, Oct. 2011. [abstract]
• S. Lahiri and S. A. Seshia, Eds., "Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT) 2011," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-80, July 2011. [abstract]
• S. A. Seshia, "Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-68, May 2011. [abstract]
• B. Brady and S. A. Seshia, "Learning Conditional Abstractions," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-24, April 2011. [abstract]
• S. K. Jha, S. A. Seshia, and A. Tiwari, "Synthesizing Switching Logic to Minimize Long-Run Cost," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-16, March 2011. [abstract]
• S. A. Seshia and A. Rakhlin, "Quantitative Analysis of Systems Using Game-Theoretic Learning," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-102, June 2010. [abstract]
• P. Nuzzo, A. A. A. Puggelli, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, "CalCS: SMT Solving for Non-linear Convex Constraints," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-100, June 2010. [abstract]
• S. K. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, "Synthesizing Switching Logic for Safety and Dwell-Time Requirements," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-28, March 2010. [abstract]
• S. K. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, "Oracle-Guided Component-Based Program Synthesis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-15, Feb. 2010. [abstract]
• D. Holcomb, W. Li, and S. A. Seshia, "Algorithms for Green Buildings: Learning-Based Techniques for Energy Prediction and Fault Diagnosis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-138, Oct. 2009. [abstract]
• J. C. Eidson, E. A. Lee, S. Matic, S. A. Seshia, and J. Zou, "Time-centric Models For Designing Embedded Cyber-physical Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-135, Oct. 2009. [abstract]
• S. A. Seshia and A. Rakhlin, "Quantitative Analysis of Embedded Software Using Game-Theoretic Learning," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-130, Sep. 2009. [abstract]
• S. K. Jha, R. S. Limaye, and S. A. Seshia, "Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-95, June 2009. [abstract]
• S. Gulwani and S. A. Seshia, Eds., "Proceedings of the 1st Workshop on Quantitative Analysis of Software (QA'09)," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-93, June 2009.
• S. K. Jha, S. A. Seshia, and R. S. Limaye, "On the Computational Complexity of Satisfiability Solving for String Theories," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2009-41, March 2009. [abstract]
• B. Brady, R. Bryant, and S. A. Seshia, "Abstracting RTL Designs to the Term Level," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2008-136, Oct. 2008. [abstract]
• O. Kupferman, W. Li, and S. A. Seshia, "On the Duality between Vacuity and Coverage," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2008-26, March 2008.
• S. K. Jha, B. Brady, and S. A. Seshia, "Symbolic Reachability Analysis of Lazy Linear Hybrid Automata," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-32, Feb. 2007. [abstract]
• S. A. Seshia, W. Li, and S. Mitra, "Verification-Guided Soft Error Resilience," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-118, Sep. 2006. [abstract]
• T. H. Feng, L. T. Wang, W. Zheng, S. Kanajan, and S. A. Seshia, "Automatic Model Generation for Black Box Real-Time Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-117, Sep. 2006. [abstract]
• S. A. Seshia, "Integrated Verification for Robust Computing," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2006-103, July 2006.
• S. A. Seshia, K. Subramani, and R. E. Bryant, "On Solving Boolean Combinations of Generalized 2SAT Constraints," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-04-179, Nov. 2004.
• V. Ganapathy, S. A. Seshia, S. Jha, T. W. Reps, and R. E. Bryant, "Automatic Discovery of API-Level Vulnerabilities," University of Wisconsin at Madison, Computer Sciences Department, Tech. Rep. UW-CS-TR-1512, July 2004.
• S. A. Seshia and R. E. Bryant, "Deciding Quantifier-Free Presburger Formulas Using Finite Instantiation Based on Parameterized Solution Bounds," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-03-210, Dec. 2003.
• R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Convergence Testing in Term-Level Bounded Model Checking," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-03-156, June 2003.
• S. A. Seshia and R. E. Bryant, "A Boolean Approach to Unbounded, Fully Symbolic Model Checking of Timed Automata," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-03-117, March 2003.
• O. Strichman, S. A. Seshia, and R. E. Bryant, "Reducing Separation Formulas to Propositional Logic," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-02-132, April 2002.
• S. A. Seshia, "Combining Thread-Modular and Procedure-Modular Verification," Compaq System Research Center, Tech. Rep. SRC-2001-004, Dec. 2001.
• S. A. Seshia, G. E. Blelloch, and R. W. Harper, "A Performance Comparison of Interval Arithmetic and Error Analysis in Geometric Predicates," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-00-172, Dec. 2000.
• S. A. Seshia and R. E. Bryant, "The Hardness of Approximating Minima in OBDDs, FBDDs and Boolean Functions," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-00-156, Aug. 2000.
• N. J. Hopper, S. A. Seshia, and J. M. Wing, "Combining Theory Generation and Model Checking for Security Protocol Analysis," Carnegie Mellon University, School of Computer Science, Tech. Rep. CMU-CS-00-107, Jan. 2000.

Unpublished articles

• R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady, "An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic (To appear)," 2008.

Ph.D. Theses

• S. A. Seshia, "Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification," Carnegie Mellon University, Department of Computer Science, May 2005.

Masters Reports

• R. S. Limaye and S. A. Seshia, "Beaver: An SMT Solver for Quantifier-free Bit-vector Logic," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2010-67, May 2010. [abstract]