# 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

- 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. [abstract] - 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

- 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. [abstract]
- S. A. Seshia, Ed., "Formal Methods for Engineering Education," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2015-170, June 2015. [abstract]
- 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. [abstract]
- 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. [abstract]
- 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. [abstract]
- A. Desai, D. Broman, J. Eidson, S. Qadeer, and S. A. Seshia, "Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems," EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-136, June 2014. [abstract]
- 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. [abstract]
- 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. [abstract]
- 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. [abstract]
- 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. [abstract]
- 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]