Shuvendu Lahiri is a 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:
- Scalable program verification in the presence of the heap
- Techniques for inferring annotations for large programs
- Logics and decision procedures for programs
- Differential static analysis of 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.
Tools/Projects
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, Mutual summaries and relative termination, no. MSR-TR-2011-112, October 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
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
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
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
PhD Thesis
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.
Tutorials
- 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.
