Shuvendu Lahiri

Awards

1. ACM SIGSOFT Distinguished Paper Award for ICSE’22 publication “TOGA: A Neural Method for Test Oracle Generation“
2. 2021 CAV award for “pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).”
3. Best paper award for “Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost” at Formal Methods in Computer Aided Design 2020
4. 10-year Most Influential Paper Award for ICSE 2007 paper “Feedback-Directed Random Test Generation” at International Conference on Software Engineering 2017
5. ACM SIGSOFT Distinguished Paper Award, “Optimizing Test Placement for Module-Level Regression Testing” International Conference on Software Engineering 2017
6. Best Paper Award, for “Wireless Protocol Validation Under Uncertainty” at the International Conference on Runtime Verification, 2016
7. ACM SIGDA 2005 Outstanding Ph.D. Dissertation Award

Press

• Interactive code generation with large language models
  • AI Helps Humans Level Up — IEEE Spectrum
  • Coding Made AI—Now, How Will AI Unmake Coding? – IEEE Spectrum
  • Will AI-automated code production make human programmers obsolete? – Dataconomy
  • Microsoft, Penn U & UC San Diego’s TiCoder Framework Generates Code With 90.4% Consistency to User Intent | Synced (syncedreview.com)
  • Researchers Develop ‘TiCoder’ Framework For Code Generation Using User Feedback With 90.4% Consistency To User Intent – MarkTechPost
  • AI tool generates code from natural language inputs – AI Business
• Future of program merges
  • Safe program merges at scale: A grand challenge for program repair research – Microsoft Research
• CAV Award
  • Former SCS Dean Randal Bryant Recognized for Contributions to Computer-Aided Verification
  • Microsoft at CAV’21
• Smart Contracts Verification
  • Researchers work to secure Azure Blockchain smart contracts with formal verification
  • Microsoft releases new tool to verify Ethereum smart contracts
  • Microsoft announces VeriSol: Ethereum smart contract verification
• Randoop
  • PATPAT: Program analysis, the practice and theory: ICSE 2017 Most Influential Paper, and supporting your research tools

Service

• Program Co-chair: CAV2020, ATVA 2018, RV 2017, SMT 2011
• Co-organizer of Dagstuhl Seminar on Program Equivalence 2018
• Program Committee member: PLDI’24, ICSE’24, MAPS’23, CAV’23, CAV’22, PLDI’22, CAV’21, POPL’20, ICSE’20, SAS’19, CAV’19, RV’18, SAS’18, CAV’18, VSTTE’17, ICSE-NIER’17, VMCAI’17, FSTTCS’16, ISEC’16, FMCAD’16, CAV’16, ICSE-NIER’16, ISEC’15, PLDI-SRC’15, SPIN’15, POPL’15 (ERC),  PLDI-SRC’14, SPIN’14, FMCAD’13, VSSE’13, SMT’12, CAV’12 (and Workshop Chair), Infinity’11, FMCAD’08, CAV’08, SMT’07, HAV’07, PDPAR’06, MEMOCODE’06.
• Thesis Committee member: Alex Gyori (UIUC), Oswaldo Olivo (UT Austin), Saikat Dutta (UIUC), Elizabeth Dinella (UPenn), Gabriel Ryan (Columbia), Rodrigo Otoni (ULugano)

Current projects

• Safe program merge (e.g., Future of Program Merge – Microsoft Research)
• Specification and Verification of Blockchain Smart Contracts (e.g. VeriSol)
• Scalable program verification for production software (e.g. Angelic Verifier)
• Differential program analysis (e.g. SymDiff project)
• Large scale modular verification of systems programs (Havoc)
• Modular reasoning about program heap (Havoc)
• Automated test generation (Randoop)
• Predicate abstraction techniques (Uclid)
• Cache coherence protocols and microprocessor verification (Uclid)
• Decision procedures and SMT solvers (Uclid)

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.

PhD Thesis