Books

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

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

• E. S. Kim, M. Arcak, and S. A. Seshia, "Symbolic control design for monotone systems with directed specifications," Automatica, vol. 83, pp. 10 - 19, Sep. 2017.
• 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.
• 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

• Y. Pant, H. Yin, M. Arcak, and S. A. Seshia, "Co-design of control and planning for multi-rotor UAVs with signal temporal logic specifications," in Proceedings of the 2021 American Control Conference, 2021, pp. 4199-4206.
• E. S. Kim, M. Arcak, and S. A. Seshia, "Flexible computational pipelines for robust abstraction-based control synthesis," in CAV 2019: Computer Aided Verification, I. Dillig and S. Tasiran, Eds., Springer International Publishing, 2019, pp. 591--608.
• E. S. Kim, M. Arcak, S. A. Seshia, B. Kim, and S. Shiraishi, "Automatic generation of communication requirements for enforcing multi-agent safety," in Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, M. Gleirscher, S. Kugele, and S. Linker, Eds., Electronic Proceedings in Theoretical Computer Science, Vol. 269, Open Publishing Association, 2018, pp. 3-16.
• E. Kim, S. Sadraddini, C. Belta, M. Arcak, and S. A. Seshia, "Dynamic contracts for distributed temporal logic control of traffic networks," in Proceedings of the 56th IEEE Conference on Decision and Control, 2017, pp. 3640-3645.
• E. S. Kim, M. Arcak, and S. A. Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts," in Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017, pp. 207--216.
• E. S. Kim, M. Arcak, and S. A. Seshia, "Directed Specifications and Assumption Mining for Monotone Dynamical Systems," in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016, pp. 21--30.
• E. Kim, M. Arcak, and S. A. Seshia, "Directed specifications and assumption mining for monotone dynamical systems," in 19th ACM International Conference on Hybrid Systems: Computation and Control, 2016, pp. 21-30.
• E. S. Kim, M. Arcak, and S. A. Seshia, "Compositional controller synthesis for vehicular traffic networks," in Decision and Control (CDC), 2015 IEEE 54th Annual Conference on, 2015, pp. 6165--6171.
• E. Kim, M. Arcak, and S. A. Seshia, "Compositional controller synthesis for vehicular traffic networks," in Proceedings of the 54th IEEE Conference on Decision and Control, 2015, pp. 6165-6171.
• D. Sadigh, E. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia, "A Learning Based Approach to Controller Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications," in 53rd IEEE Conference on Decision and Control, 2014.
• C. Sturton, R. Sinha, T. Dang, S. Jain, M. McCoyd, W. Y. Tan, P. Maniatis, S. A. Seshia, and D. Wagner, "Symbolic Software Model Validation," in Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), M. Roncken and J. Talpin, Eds., 2013.
• W. Li, A. Gascon, P. Subramanyan, W. Y. Tan, A. Tiwari, S. Malik, N. Shankar, and S. A. Seshia, "WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates," in IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), 2013.
• 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

• D. Dalrymple, J. Skalse, Y. Bengio, S. J. Russell, M. Tegmark, S. A. Seshia, S. Omohundro, C. Szegedy, A. Abate, J. Halpern, C. Barrett, D. Zhao, B. Goldhaber, and N. Ammann, "Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2024-45, May 2024.
• E. Kim, A. Sturgis, Z. Pardos, K. Cui, J. Hu, Y. Xiao, B. Fu, D. He, I. Gonzalez, A. L. Sangiovanni-Vincentelli, S. A. Seshia, and B. Hartmann, "Task Distribution Aware Psychomotor Skill Training with Probabilistic Programs and Bayesian Knowledge Tracing in Virtual Reality," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2024-16, April 2024.
• V. Tuck, P. Chen, G. Fainekos, B. Hoxha, H. Okamoto, S. S. Sastry, and S. A. Seshia, "SMT-Based Dynamic Multi-Robot Task Allocation," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2024-12, March 2024.
• S. Bhatia, J. Qiu, S. A. Seshia, and A. Cheung, "Can LLMs Perform Verified Lifting of Code?," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2024-11, March 2024.
• A. Godbole, K. Cheang, Y. Manerkar, and S. A. Seshia, "Specifying and Generating Abstract Models for Formal Security Analysis," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2023-230, Sep. 2023.
• K. Cheang, A. Godbole, Y. A. Manerkar, and S. A. Seshia, "Compositional Proofs of Information Flow Properties for Hardware-Software Platforms," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2023-204, Aug. 2023.
• J. Wong, P. Chen, T. Zhang, J. Gonzalez, Y. Tian, and S. A. Seshia, "Ashera; Neural Guided Optimization Modulo Theory," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2023-103, May 2023.
• E. Kim, Z. Pardos, S. A. Seshia, and B. Hartmann, "A Principled Intelligent Occupational Training of Psychomotor Skills in Virtual Reality," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2023-17, Feb. 2023.
• I. Incer, A. Benveniste, R. M. Murray, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, "Algorithms for Context-Aided Variable Elimination," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2023-15, Jan. 2023.
• I. Incer, A. Benveniste, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, "Hypercontracts," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2021-158, May 2021.
• E. Polgreen, A. Reynolds, and S. A. Seshia, "Satisfiability and Synthesis Modulo Oracles," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2021-10, April 2021.
• Y. V. Pant, B. Thoravi Kumaravel, A. Shah, E. Kraemer, M. Vazquez-Chanlatte, K. Kulkarni, B. Hartmann, and S. A. Seshia, "Model-based Formalization of the Autonomy-to-Human Perception Hand-off," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2021-8, March 2021.
• M. Weber, B. Jin, G. Lederman, Y. Shoukry, E. A. Lee, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, "Gordian: Formal Reasoning Based Outlier Detection for Secure Localization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2019-1, Jan. 2019.
• A. Desai, S. Ghosh, S. A. Seshia, N. Shankar, and A. Tiwari, "Soter: Programming Safe Robotics System using Runtime Assurance," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2018-127, Aug. 2018.
• A. Desai, A. Phanishayee, S. Qadeer, and S. A. Seshia, "Compositional Programming and Testing of Dynamic Distributed Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2018-95, July 2018.
• S. A. Seshia, A. Desai, T. Dreossi, D. Fremont, S. Ghosh, E. Kim, S. Shivakumar, M. Vazquez-Chanlatte, and X. Yue, "Formal Specification for Deep Neural Networks," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2018-25, May 2018.
• D. Fremont, X. Yue, T. Dreossi, S. Ghosh, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, "Scenic: Language-Based Scene Generation," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2018-8, April 2018.
• T. Dreossi, A. Donze, and S. A. Seshia, "Compositional Falsification of Cyber-Physical Systems with Machine Learning Components," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2017-165, Nov. 2017.
• S. A. Seshia, "Compositional Verification without Compositional Specification for Learning-Based Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2017-164, Nov. 2017.
• R. Sinha, S. Rajamani, and S. A. Seshia, "A Compiler and Verifier for Page Access Oblivious Computation," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2017-124, July 2017.
• M. Weber, B. Jin, G. Lederman, Y. Shoukry, E. A. Lee, S. A. Seshia, and A. L. Sangiovanni-Vincentelli, "Gordian SMT: Untangling Ranging Attacks in Noisy Sensor Networks for Secure Localization," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2017-5, March 2017.
• D. J. Fremont, M. N. Rabe, and S. A. Seshia, "Maximum Model Counting," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2016-169, Nov. 2016.
• T. Yamaguchi, T. Kaga, A. Donze, and S. A. Seshia, "Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2016-124, June 2016.
• A. Desai, E. Jackson, A. Phanishayee, S. Qadeer, and S. A. Seshia, "Building Reliable Distributed Systems With P," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-198, Sep. 2015.
• S. A. Seshia, Ed., "Formal Methods for Engineering Education," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-170, June 2015.
• R. Sinha, S. Rajamani, S. A. Seshia, and K. Vaswani, "Verification of Confidentiality Properties of Enclave Programs," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-162, June 2015.
• A. Desai, S. A. Seshia, S. Qadeer, D. Broman, and J. Eidson, "Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-158, May 2015.
• D. Sadigh, E. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia, "A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-166, Sep. 2014.
• D. Broman, P. Derler, A. Desai, J. Eidson, and S. A. Seshia, "Endlessly Circulating Messages in IEEE 1588-2008 Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-62, May 2014.
• A. A. A. Puggelli, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, "Robust Strategy Synthesis for Probabilistic Systems Applied to Risk-Limiting Renewable-Energy Pricing," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-16, Feb. 2014.
• D. Sadigh, K. Driggs Campbell, A. A. A. Puggelli, W. Li, V. Shia, R. Bajcsy, A. L. Sangiovanni-Vincentelli, S. S. Sastry, and S. A. Seshia, "Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2013-197, Dec. 2013.
• A. Donze, S. Libkind, S. A. Seshia, and D. Wessel, "Control Improvisation with Application to Music," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2013-183, Nov. 2013.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• B. Brady and S. A. Seshia, "Learning Conditional Abstractions," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-24, April 2011.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

Patents

• J. V. Deshmukh, X. Jin, A. Donze, and S. A. Seshia, "Systems and methods for mining temporal requirements from block diagram models of control systems," U.S. Patent 9,081,900. July 2015.

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.