Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Shuvendu Lahiri

Shuvendu Lahiri
SENIOR RESEARCHER
.

Shuvendu Lahiri is a Senior Researcher in the Research in Software Engineering (RiSE) Group.

I am interested in the development and the application of rigorous techniques for making program testing, verification and review more scalable and automated.

Current projects:

Earlier projects:

In my earlier life, I was a graduate student at Carnegie Mellon University. Before that, I spent four wonderful years at the Computer Science and Engineering Dept. at the Indian Institute of Technology, Kharagpur.

Tools/Projects

    • Techniques for differential program verification
    • Customizable, heap-aware extended static checking for large C/C++ codebases
    • A whole program verifier based on model checking
    • Feedback-directed random testing
Publications

2015

Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li, Angelic Verification: Precise Verification Modulo Unknowns, in Computer Aided Verification (CAV), Springer, July 2015.

Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel, Automatic Rootcausing for Program Equivalence Failures in Binaries, in Computer Aided Verification (CAV'15), Springer, July 2015.

Michael Barnett, Christian Bird, Joao Brunet, and Shuvendu Lahiri, Helping developers help themselves: Automatic decomposition of code review changesets., in Proceedings of the 37th International Conference on Software Engineering, IEEE – Institute of Electrical and Electronics Engineers, May 2015.

Arvind Haran, Shuvendu K. Lahiri, Zvonimir Rakamaric, and Ganesh Gopalakrishnan, Differential Program Verification for Approximate Computing, 1 February 2015.

2014

Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear, Verification Modulo Versions: Towards Usable Verification, in Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014), ACM SIGPLAN, June 2014.

Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel, Automatic Rootcausing for Program Equivalence Failures in Binaries, no. MSR-TR-2014-11, February 2014.

2013

Shuvendu Lahiri, Ken McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, in Foundations of Software Engineering (FSE'13), ACM, August 2013.

Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, and Scott Wadsworth, Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation, in Foundations of Software Engineering (FSE'13), ACM, August 2013.

Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebelo, Towards Modularly Comparing Programs using Automated Theorem Provers, in International Conference on Automated Deduction (CADE '13), Springer, June 2013.

Sam Blackshear and Shuvendu Lahiri, Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings, in Programming Language Design and Implementation (PLDI'13), ACM, June 2013.

Julien Vanegue and Shuvendu Lahiri, Towards practical reactive security audit using extended static checkers, in IEEE Symposium on Security and Privacy (Oakland'13), May 2013.

2012

Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, in Computer-Aided Verification (CAV), July 2012.

Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebelo, SymDiff: A language-agnostic semantic diff tool for imperative programs, in Computer Aided Verification (CAV '12) (Tool description), Springer, July 2012.

Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012.

Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, no. MSR-TR-2012-9, January 2012.

2011

Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Towards Modularly Comparing Programs using Automated Theorem Provers, no. MSR-TR-2011-112, October 2011.

Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Mutual Summaries: Unifying Program Comparison Techniques, no. MSR-TR-2011-78, August 2011.

Patrice Godefroid, Shuvendu Lahiri, and Cindy Rubio-González, Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation, in Static Analysis Symposium (SAS '11), Lecture Notes in Computer Science, August 2011.

Shuvendu K. Lahiri, Shaz Qadeer, and David Walker, Linear Maps, in ACM SIGPLAN Workshop on Programming Languages meets Program Verification, ACM SIGPLAN, January 2011.

2010

Shuvendu K. Lahiri, Kapil Vaswani, and Tony Hoare, Differential Static Analysis: Opportunities, Applications, and Challenges, in 2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) , Association for Computing Machinery, Inc., November 2010.

Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebelo, Conditional equivalence, no. MSR-TR-2010-119, October 2010.

Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, and Julien Vanegue, Towards scalable modular checking of user-defined properties, in Verified Software: Theories, Tools and Experiments (VSTTE 2010), Springer Verlag, August 2010.

Shuvendu K. Lahiri and Julien Vanegue, ExplainHoudini: Making Houdini inference transparent, no. MSR-TR-2010-118, August 2010.

Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-Gonzalez, Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation, no. MSR-TR-2010-11, February 2010.

Shuvendu Lahiri, Alexander Malkis, and Shaz Qadeer, Abstract Threads, in Conference on Verification, Model Checking, and Abstract Interpretation, Springer Verlag, January 2010.

2009

Shuvendu K. Lahiri and Shaz Qadeer, Call invariants, no. MSR-TR-2009-13, July 2009.

Shuvendu K. Lahiri and Shaz Qadeer, Complexity and algorithms for monomial and clausal predicate abstraction, in International Conference on Automated Deduction (CADE '09), Springer Verlag, March 2009.

Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009.

Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, and Thomas Wies, Intra-Module Inference, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009.

Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer, Unifying Type Checking and Property Checking for Low-Level Code, in Principles of Programming Languages (POPL '09), Association for Computing Machinery, Inc., January 2009.

2008

Carlos Pacheco, Shuvendu Lahiri, and Thomas Ball, Finding Errors in .NET with Feedback-Directed Random Testing, in International Symposium on Software Testing and Analysis (ISSTA '08), Association for Computing Machinery, Inc., July 2008.

Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, and Thomas Ball, Towards scalable modular checking of user-defined properties, no. MSR-TR-2008-82, May 2008.

Shuvendu Lahiri and Shaz Qadeer, Back to the Future: Revisiting Precise Program Verification using SMT Solvers, in Principles of Programming Languages (POPL '08), Association for Computing Machinery, Inc., January 2008.

2007

Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball, Feedback-Directed Random Test Generation, in International Conference on Software Engineering (ICSE '07), IEEE Computer Society, September 2007.

Shuvendu Lahiri and Krishna Kumar Mehra, Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic, in Journal on Satisfiability, Boolean Modeling and Computation (JSAT '07), no. MSR-TR-2005-121, pp. 0, September 2007.

Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, A Reachability Predicate for Analyzing Low-Level Software, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS '07), Springer Verlag, April 2007.

Shuvendu K. Lahiri, Thomas Ball, and Byron Cook, Predicate Abstraction via Symbolic Decision Procedures, in Logical Methods in Computer Science (LMCS '07), vol. 3, no. 2, 2007.

Shuvendu K. Lahiri and Randal E. Bryant, Predicate abstraction with indexed predicates, in ACM Transactions on Computational Logic (TOCL '07), vol. 9, no. 1, Association for Computing Machinery, Inc., 2007.

2006

Shuvendu K. Lahiri and Shaz Qadeer, Verifying properties of well-founded linked lists, in Principles of Programming Languages (POPL '06), ACM, 2006.

Shuvendu K. Lahiri and Madanlal Musuvathi, An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals, in Electr. Notes Theor. Comput. Sci., vol. 144, no. 2, pp. 27-41, Elsevier , 2006.

Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras, SMT Techniques for Fast Predicate Abstraction, in Conference on Computer Aided Verification (CAV '06), Springer, 2006.

Shuvendu K. Lahiri and Madanlal Musuvathi, Solving Sparse Linear Constraints, in Automated Reasoning, Third International Joint Conference (IJCAR '06), Springer, 2006.

2005

Thomas Ball, Shuvendu Lahiri, and Madanlal Musuvathi, Zap: Automated Theorem Proving for Software Analysis, in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05), Springer Verlag, October 2005.

Shuvendu Lahiri and Madanlal Musuvathi, An Efficient Decision Procedure for UTVPI Constraints, in Frontiers of Combining Systems (FroCos '05), Springer Verlag, May 2005.

Shuvendu Lahiri, Thomas Ball, and Byron Cook, Predicate Abstraction via Symbolic Decison Procedures, in Computer Aided Verification (CAV '05), Springer Verlag, April 2005.

Tutorials

  • Email: com\microsoft\shuvendu
  • Phone: 425-722-4122
  • Fax:    425-936-7329
  • Mail: One Microsoft Way, Redmond, WA 98052