Faculty Publications - Sanjit A. Seshia

Books

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

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

Unpublished articles

Patents

Ph.D. Theses

Masters Reports