Publications

My Erdos number is 4.         Here is my DBLP entry.

Notice:The documents referenced on this page are included by the contributing authors as a means to ensure timely dissemination of technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's or owner's copyright. 

Contents:

(Papers listed in reverse chronological order; click on title for electronic copy in postscript or pdf format.)

Most recent publications:

Refereed Conferences/Workshops
 

On Voting Machine Design for Verification and Testability
Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, and David Wagner
In ACM Conference on Computer and Communications Security (CCS), November 2009, to appear.

 
Localizing Transient Faults Using Dynamic Bayesian Networks
Susmit Jha, Wenchao Li, and Sanjit A. Seshia
In IEEE International High Level Design Validation and Test Workshop (HLDVT), November 2009, to appear.

 
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
Susmit Jha, Rhishikesh Limaye, and Sanjit A. Seshia.
In Computer-Aided Verification (CAV), June 2009.

 
Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits
Daniel Holcomb, Wenchao Li, and Sanjit A. Seshia.
In Design, Automation and Test in Europe (DATE), April 2009.

 
Optimizations of an Application-Level Protocol for Enhanced Dependability in FlexRay
Wenchao Li, Marco Di Natale, Wei Zheng, Paolo Giusto, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia.
In Design, Automation and Test in Europe (DATE), April 2009..

 
Game-Theoretic Timing Analysis
Sanjit A. Seshia and Alexander Rakhlin
In IEEE/ACM Conference on Computer-Aided Design (ICCAD), November 2008.

 
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
Orna Kupferman, Wenchao Li, and Sanjit A. Seshia
In IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2008.

 
Effective Blame for Information-Flow Violations
Dave King, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia
In ACM Conference on Foundations of Software Engineering (FSE), November 2008.

 
Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
Susmit Jha, Bryan Brady, and Sanjit A. Seshia
In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), October 2007, pages 241-256.

 
An Application of Web-Service Interfaces
Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, and Sanjit A. Seshia.
In Proc. International Conference on Web Services (ICWS), July 2007.

 
Autonomic Reactive Systems via Online Learning
Sanjit A. Seshia.
In Proc. International Conference on Autonomic Computing (ICAC), June 2007.

 
Sketching Stencils
Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit A. Seshia.
In Proc. International Conference on Programming Languages Design and Implementation (PLDI), June 2007.

 
Verification-Guided Soft Error Resilience
Sanjit A. Seshia, Wenchao Li, and Subhasish Mitra.
In Proc. Design Automation and Test in Europe (DATE), April 2007, pages 1442-1447.

 
Automatic Model Generation for Black Box Real-Time Systems
Huining Thomas Feng, Lynn Tao-Ning Wang, Wei Zheng, Sri Kanajan and Sanjit A. Seshia.
In Proc. Design Automation and Test in Europe (DATE), April 2007, pages 930-935.

 
Deciding Bit-Vector Arithmetic with Abstraction
Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady.
In 13th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 358-372, March 2007.

 
Combinatorial Sketching for Finite Programs
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit A. Seshia.
In 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 404-415, ACM Press, 2006.

 
Semantics-Aware Malware Detection.
Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Song, and Randal E. Bryant.
IEEE Symposium on Security and Privacy, Oakland, May 2005, pages 32-46.

 
Automatic Discovery of API-Level Exploits.
Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, and Randal E. Bryant.
27th International Conference on Software Engineering (ICSE), May 2005, pages 312-321.

 
Modeling and Verifying Circuits Using Generalized Relative Timing.
Sanjit A. Seshia, Randal E. Bryant, and Kenneth S. Stevens.
11th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), March 2005, pages 98-108.

 
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds.
Sanjit A. Seshia and Randal E. Bryant.
Proc. of 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 100-109, July 2004.

 
Abstraction-Based Satisfiability Solving of Presburger Arithmetic.
Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, and Ofer Strichman.
Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 308-320, July 2004.

 
The UCLID Decision Procedure.
Shuvendu K. Lahiri and Sanjit A. Seshia.
Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 475-478, July 2004.

 
Convergence Testing in Term-Level Bounded Model Checking.
Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.
12th Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 2860, pages 348-362, October 2003.

 
Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods.
Sanjit A. Seshia and Randal E. Bryant.
In Proc. Intl. Conf. on Computer-Aided Verification (CAV), LNCS 2725, pages 154-166, July 2003.

 
A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions.
Sanjit A. Seshia, Shuvendu K. Lahiri, and Randal E. Bryant.
In Proc. 40th Design Automation Conference (DAC), ACM Press, pages 425-430, June 2003.

 
Modeling and Verification of Out-of-Order Microprocessors Using UCLID.
Shuvendu K. Lahiri, Sanjit A. Seshia, and Randal E. Bryant.
In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 142-159, November 2002.

 
Deciding CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings.
Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.
In Proc. Intl. Workshop on Constraints in Formal Verification ,September 2002. Associated with Intl. Conf. on Principles and Practice of Constraint Programming.

 
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.
Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia.
In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002.

 
Deciding Separation Formulas with SAT.
Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant.
In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002.

 
A Modular Checker for Multithreaded Programs.
Cormac Flanagan, Shaz Qadeer and Sanjit A. Seshia.
In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002.

 
A Comparison and Combination of Theory Generation and Model Checking for Security Protocol Analysis.
Nicholas J. Hopper, Sanjit A. Seshia, Jeannette M. Wing.
In Workshop on Formal Methods in Computer Security (FMCS), July 2000. Chicago. Associated with Intl. Conf. on Computer-Aided Verification (CAV'00).

 
A Translation of Statecharts to Esterel.
S. A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee and S. D. Dhodapkar.
In Proceedings of the World Congress on Formal Methods, FM'99, Toulouse, France, LNCS vol. 1709, Sept. 1999, pp.983-1007.

 
A Graphical Environment for the Specification and Verification of Reactive Systems.
A.K. Bhattcharjee, S.D. Dhodapkar, S.A. Seshia and R.K. Shyamasundar.
In Proceedings of SAFECOMP'99, Toulouse, France. LNCS vol. 1698, Sept. 1999, pp. 431-444.

 

 
 

Journals
 

An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic
Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady
Software Tools for Technology Transfer (STTT), to appear.

 
On Solving Boolean Combinations of UTVPI Constraints
Sanjit A. Seshia, K. Subramani, and Randal E. Bryant
Journal on Satisfiability, Boolean Modeling and Computation, 2007.

 
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
Sanjit A. Seshia and Randal E. Bryant
Logical Methods in Computer Science, vol. 1 (2:6), December 19, 2005, pp. 1-26.

 
Modular Verification of Multithreaded Programs.
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer and Sanjit A. Seshia.
Theoretical Computer Science, Volume 338, Issues 1-3, 10 June 2005, pp. 153-183.

 
PERTS: A graphical environment for the specification and verification of reactive systems.
A.K. Bhattcharjee, S.D. Dhodapkar, S.A. Seshia and R.K. Shyamasundar.
Journal of Reliability Engineering and System Safety, 71 (3), 2001, pp. 299 -310 , Elsevier Science.(corrigendum in vol. 72(2), pp. 223)

 

 
 

Book Chapters / Ph.D. Thesis
 

Satisfiability Modulo Theories
Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli.
Chapter 8 in the Handbook of Satisfiability, Armin Biere, Hans van Maaren, and Toby Walsh, editors, IOS Press, 2009.

 
Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification.
Sanjit A. Seshia.
Ph.D. Thesis, Carnegie Mellon University, May 2005.
Co-winner, 2005 SCS Distinguished Dissertation Award.

 

Technical Reports
  (a bit out of date, please see my CV for the up-to-date list)

On Solving Boolean Combinations of Generalized 2SAT Constraints.
Sanjit A. Seshia, K. Subramani, and Randal E. Bryant.
Computer Science Department Technical report CMU-CS-04-179, November 2004.

 
Automatic Discovery of API-Level Vulnerabilities.
Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant.
Technical report UW-CS-TR-1512, Computer Sciences Department, University of Wisconsin, Madison, July 2004.

 
Deciding Quantifier-Free Presburger Formulas Using Finite Instantiation Based on Parameterized Solution Bounds.
Sanjit A. Seshia and Randal E. Bryant.
Computer Science Department Technical report CMU-CS-03-210, December 2003.

 
Convergence Testing in Term-Level Bounded Model Checking
R. E. Bryant, S. K. Lahiri, and S. A. Seshia.
Computer Science Department Technical report CMU-CS-03-156, June 2003.

 
A Boolean Approach to Unbounded, Fully Symbolic Model Checking of Timed Automata.
S. A. Seshia, and R. E. Bryant.
Computer Science Department Technical report CMU-CS-03-117, March 2003.

 
Reducing Separation Formulas to Propositional Logic.
O. Strichman, S. A. Seshia, and R. E. Bryant.
Computer Science Department Technical report CMU-CS-02-132, April 2002.

 
Combining Thread-Modular and Procedure-Modular Verification.
S. A. Seshia
In Compaq Systems Research Center Technical note SRC-2001-004, December 2001.

 
A Performance Comparison of Interval Arithmetic and Error Analysis in Geometric Predicates.
S. A. Seshia, G. E. Blelloch and R. W. Harper.
Computer Science Department Technical report CMU-CS-00-172, December 2000.

 
The Hardness of Approximating Minima in OBDDs, FBDDs and Boolean functions.
S. A. Seshia and R. E. Bryant.
Computer Science Department technical report CMU-CS-00-156, August 2000.

 
Combining Theory Generation and Model Checking for Security Protocol Analysis.
Nicholas J. Hopper, Sanjit A. Seshia, Jeannette M. Wing.
Computer Science Department technical report CMU-CS-00-107, January 2000.

 

Co-authors  (listed in alphabetical order)