SRR | SWIG | MSR | Microsoft

home | current research | people | search | news | publications | downloads | opportunities | labs | visit msr

E-mail	\com\microsoft\shuvendu
Office:	(425) 722-4122
FAX:	(425) 936-7329
Mail:	One Microsoft Way, Redmond, WA 98052

Shuvendu Lahiri is a Researcher in the Software Reliability Research Group.

I am interested in the development and the application of symbolic techniques for making testing and verification more scalable and automated. Currently my focus lies in the following ideas:

• Decision procedures and theorem-provers for program analysis
• Abstraction techniques for software and hardware
• Analyzing heap manipulating programs
• Testing object-oriented software

I am currently mostly involved with the HAVOC project. Previously, I worked on the Zap, and MUTT projects.

In my earlier life, I was a graduate student at Carnegie Mellon University. My old page has some more information about me.

Biography

Shuvendu K. Lahiri is a Researcher in the Software Reliability Research group at Microsoft Research, Redmond. He obtained a M.S. and a Ph.D. in Computer Engineering from Carnegie Mellon University in 2001 and 2004 respectively. Earlier, he obtained his B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Kharagpur in 1999. He is currently interested in decision procedures, abstraction mechanisms and symbolic reasoning for verifying and testing of software. His Ph.D. dissertation "Unbounded System Verification using Decision Procedure and Predicate Abstraction" won the 2004-2005 ACM (SIGDA) Outstanding Ph.D. Dissertation in Electronic Design Automation.

Professional service

• Program Committee, Formal Methods in Computer-Aided Design 2008 (FMCAD '08)
• Program Committee, Computer Aided Verification 2008 (CAV '08)
• Program Committee, Workshop on Satisfiability Modulo Theories 2007 (SMT '07)
• Program Committee, Heap Analysis and Verification 2007 (HAV '07)
• Program Committee, Pragmatics of Decision Procedures in Automated Reasoning 2006 (PDPAR '06)
• Program Committee, International Conference on Formal Methods and Models for Codesign 2006 (MEMOCODE '06)
  

Publications

Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer
(Preliminary) Microsoft Research Technical Report MSR-TR-2008-96, July 2008.
In Proceedings of the 36rd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL), 2009.

Annotation-based property checking for systems software
Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer
Microsoft Research Technical Report MSR-TR-2008-82, May 2008

"Finding Errors in .NET with Feedback-Directed Random Testing"
Carlos Pacheco, Shuvendu K. Lahiri, Thomas Ball.
 In Proceedings of International Symposium on Software Testing and Analysis (ISSTA), July 2008  

"Back to the Future: Revisiting Precise Program Verification using SMT Solvers."
Shuvendu K. Lahiri, Shaz Qadeer, (Preliminary) Microsoft Research Technical Report MSR-TR-2007-88, July 2007.
In Proc. of The 35rd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages 2008 (POPL 2008), San Francisco, CA.

"Feedback-directed Random Test Generation"
Carlos Pacheco, Shuvendu K. Lahiri, Michael Ernst, Thomas Ball.
 In Proceedings of the 29th International Conference on Software Engineering (ICSE '07), (Minneapolis, MN, USA), May 2007  

"A Reachability Predicate for Analyzing Low-Level Software"
Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer and Zvonimir Rakamaric.
 In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '07), Portugal, March 2007
 [Benchmarks]

"Indexed Predicate Discovery for Unbounded System Verification"
Shuvendu K. Lahiri, Randal E. Bryant
In Proc. of  Computer-Aided Verification (CAV 04), Boston, July 2004

"Zapato: Automatic theorem proving for predicate abstraction refinement"
Thomas Ball, Byron Cook, Shuvendu K. Lahiri and  Lintao Zhang
(Tool Description) In Proc. of  Computer-Aided Verification (CAV 04), Boston, July 2004

"The UCLID Decision Procedure"
Shuvendu K. Lahiri, Sanjit A. Seshia
(Tool Description) In Proc. of  Computer-Aided Verification (CAV 04), Boston, July 2004

"Revisiting Positive Equality"
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel and Muralidhar Talupur
In Proc. of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Barcelona, March 2004

"Constructing Quantified Invariants via Predicate Abstraction"
Shuvendu K. Lahiri and Randal E. Bryant
In Proc. of  5th Intl. Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), LNCS  2937, Springer-Verlag, Pages 267-281, Venice, Italy, January 2004.

"Convergence Testing in Term-level Bounded Model Checking"
Randal E. Bryant, Shuvendu K. Lahiri and Sanjit A. Seshia.
In Proc. of  12th Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS  2860, Springer-Verlag, Pages 348-362,  L'Aquila, Italy, October 2003.

"A Symbolic Approach to Predicate Abstraction"
Shuvendu K. Lahiri, Randal  E. Bryant and Byron Cook. 
In Proc. of Computer-Aided Verification (CAV 03), LNCS  2725, Springer-Verlag, Pages 141-153, Colorado, USA, July 2003

"Deductive Verification of Advanced Out-of-Order Microprocessors"
Shuvendu K. Lahiri and Randal E. Bryant.
In Proc. of Computer-Aided Verification (CAV 03), LNCS  2725, Springer-Verlag, Pages 341-354, Colorado, USA, July 2003  

"A Hybrid SAT-based Decision Procedure for Separation Logic with Uninterpreted Functions"
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant. 
In Proc. Design Automation Conference (DAC '03),  ACM Press, Pages: 425 - 430, Anaheim, CA, USA,  June 2003

"Modeling and Verification of Out-of-order Microprocessors in UCLID"
Shuvendu K. Lahiri, Sanjit A. Seshia, and Randal E. Bryant.
In Proc. International  Conference on Formal Methods in Computer-Aided Design (FMCAD '02), LNCS 2517, Springer-Verlag, Pages 142 - 158, Portland, USA,  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 '02), LNCS 2404,  Springer-Verlag, Pages 78 - 92, Copenhagen, Denmark, July 2002

PhD Thesis

 "Unbounded System Verification using Decision Procedure and Predicate Abstraction", PhD Thesis, Electrical and Computer Engineering Department, Carnegie Mellon University, Pittsburgh, PA, September 2004. Winner of the 2004-2005 ACM (SIGDA) Outstanding Ph.D. Dissertation in Electronic Design Automation.

Software Reliability Research