Shuvendu Lahiri is a Senior Researcher in the Research in Software Engineering (RiSE) Group.
I am interested in the development and the application of symbolic techniques for making testing and verification more scalable and automated with low false-alarms. Currently my focus lies in the following ideas:
- Differential program analysis
- Semantic techniques to assign confidence to program verification warnings
- Scalable program verification in the presence of the heap
- Techniques for inferring annotations for large programs
- Logics and decision procedures for programs
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.
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
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
Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, no. MSR-TR-2013-34, March 2013
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
Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, no. MSR-TR-2012-9, January 2012
Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Towards Modularly Comparing Programs using Automated Theorem Provers, no. MSR-TR-2011-112, October 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
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Mutual Summaries: Unifying Program Comparison Techniques, no. MSR-TR-2011-78, 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
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
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
Unbounded System Verification using Decision Procedure and Predicate Abstraction. Carnegine Mellon University, 2004. Winner to the ACM Outstanding Ph.D. Dissertation Award in Electronic Design Automation.
- iFM 2009 Tutorial: Contract Specification and Checking: Application to .NET and C. Together with Francesco Logozzo.
- CADE 2009 Tutorial on HAVOC: Precise, Automated and Scalable Verification of Systems Software using SMT solvers. Together with Shaz Qadeer.