- Trusted AI-assisted programming Trusted AI-assisted Programming – Microsoft Research
Activities
Awards
- ACM SIGSOFT Distinguished Paper Award (opens in new tab) for ICSE’22 publication “TOGA: A Neural Method for Test Oracle Generation“
- 2021 CAV award (opens in new tab) for “pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).”
- Best paper award (opens in new tab) for “Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost” at Formal Methods in Computer Aided Design 2020
- 10-year Most Influential Paper Award for ICSE 2007 paper (opens in new tab)“Feedback-Directed Random Test Generation” at International Conference on Software Engineering 2017
- ACM SIGSOFT Distinguished Paper Award (opens in new tab), “Optimizing Test Placement for Module-Level Regression Testing” International Conference on Software Engineering 2017
- Best Paper Award, for “Wireless Protocol Validation Under Uncertainty” at the International Conference on Runtime Verification, 2016
- ACM SIGDA 2005 Outstanding Ph.D. Dissertation Award (opens in new tab)
Press
- Interactive code generation with large language models
- AI Helps Humans Level Up — IEEE Spectrum (opens in new tab)
- Coding Made AI—Now, How Will AI Unmake Coding? – IEEE Spectrum (opens in new tab)
- Will AI-automated code production make human programmers obsolete? – Dataconomy (opens in new tab)
- Microsoft, Penn U & UC San Diego’s TiCoder Framework Generates Code With 90.4% Consistency to User Intent | Synced (syncedreview.com) (opens in new tab)
- Researchers Develop ‘TiCoder’ Framework For Code Generation Using User Feedback With 90.4% Consistency To User Intent – MarkTechPost (opens in new tab)
- AI tool generates code from natural language inputs – AI Business (opens in new tab)
- Future of program merges
- CAV Award
- Smart Contracts Verification
- Randoop
Service
- Program Co-chair: CAV2020 (opens in new tab), ATVA 2018 (opens in new tab), RV 2017 (opens in new tab), SMT 2011 (opens in new tab)
- Co-organizer of Dagstuhl Seminar on Program Equivalence 2018 (opens in new tab)
- 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 (opens in new tab)(UIUC), Oswaldo Olivo (UT Austin), Saikat Dutta (opens in new tab) (UIUC), Elizabeth Dinella (opens in new tab) (UPenn), Gabriel Ryan (opens in new tab) (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 (opens in new tab))
- Decision procedures and SMT solvers (Uclid (opens in new tab))
In my earlier life, I was a graduate student at Carnegie Mellon University (opens in new tab). Before that, I spent four wonderful years at the Computer Science and Engineering Dept. at the Indian Institute of Technology, Kharagpur (opens in new tab).
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. (opens in new tab)
Tutorials
- Tutorial slides on differential program verification at the Halmstad Summer School on Testing, 2015 (opens in new tab)
- iFM 2009 Tutorial: Contract Specification and Checking: Application to .NET and C. (opens in new tab) Together with Francesco Logozzo.
- CADE 2009 Tutorial on HAVOC: Precise, Automated and Scalable Verification of Systems Software using SMT solvers. Together with Shaz Qadeer.