Shuvendu Lahiri

About

I am a Senior Principal Researcher in the Research in Software Engineering (RiSE) Group. I am interested in the development and the application of rigorous techniques rooted in formal methods and (of late) machine learning for reliable software development (program analysis, formal verification, test generation, program integration, synthesis). Earlier, I obtained my PhD from Carnegie Mellon University, and my B.Tech. from Indian Institute of Technology, Kharagpur, India.

I have been fortunate to contribute to the development of several tools based on formal methods and rigorous foundations that have been shipped externally or used by product groups to improve the quality of their products. A few notable ones:

1. Randoop (one of the first scalable automated test generation tool) was used extensively by the .NET CLR team for testing the libraries
2. HAVOC (first scalable extended static checker for C/C++) was used extensively by MSEC team to find variants of security vulnerabilities in Internet Explorer and Windows
3. SymDiff (first semantic diff tool for real-world programs) was used extensively by the CLR JIT compiler team to test for binary compatibility of .NET JIT compiler across version upgrades
4. Angelic Verification (first automated static verifier for open programs) was used by Windows Driver Quality Team and shipped through the Static Driver Verifier tool
5. VeriSol (first automated whole program verifier for Solidity smart contracts) was used extensively by the Azure Blockchain team to develop and verify production grade smart contracts
6. MrgBldBrkFixer (first tool for rootcausing and fixing merge-induced build breaks) components were used by the Microsoft Edge engineering team for rootcausing merge-induced build breaks