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 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
- Analyzing heap manipulating programs
- Logics and decision procedures for programs
I am currently 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. Before that, I spent four wonderful years at the Computer Science and Engineering Dept. at the Indian Institute of Technology, Kharagpur.
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, Juan P. Galeotti, Jan W. Voung, and Thomas Wies, Intra-Module Inference, in Computer Aided Verification (CAV '09), Springer Verlag, February 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
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, Scalable Modular Checking of System-Specific Properties: Myth or Reality?, 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 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
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
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 and Madanlal Musuvathi, Solving Sparse Linear Constraints, in Automated Reasoning, Third International Joint Conference (IJCAR '06), Springer, 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
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
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.
