3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Shuvendu Lahiri
Senior Principal Researcher
Publications
Publications by Year
-
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
-
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
October 2024
Leveraging LLMs for Program Verification
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma
Formal Methods in Computer-Aided Design (FMCAD) | October 2024
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
September 2024
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu Lahiri
The ACM International Conference on the Foundations of Software Engineering (FSE) | July 2024
GitHub page https://github.com/microsoft/nl-2-postcond/
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
Formal Methods in Computer-Aided Design (FMCAD'24) | July 2024
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Shuvendu Lahiri
IEEE Transactions on Software Engineering | April 2024, Vol 50: pp. 2254-2268
-
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
Inference of Resource Management Specifications
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, Manu Sridharan
OOPSLA | October 2023
Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context
Lakshya A Agrawal, Aditya Kanade, Navin Goyal, Shuvendu Lahiri, Sriram Rajamani
NeurIPS 2023 | June 2023
Preprint
CODAMOSA: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models
Caroline Lemieux, Jeevana Priya Inala, Shuvendu Lahiri, Siddhartha Sen
ICSE'23 | May 2023
-
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Sarah Fakhoury, Negar Ghorbani, Todd Mytkowicz, Christian Bird, Jinu Jang, Neel Sundaresan, Shuvendu Lahiri, Elizabeth Dinella
The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '22) | November 2022
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
IEEE Transactions on Software Engineering (TSE'22) | July 2022
Using Pre-trained Language Models to Resolve Textual and Semantic Merge Conflicts (Experience Paper)
Jialu Zhang, Mike Kaufman, Todd Mytkowicz, Ruzica Piskac, Shuvendu Lahiri
ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis | July 2022
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript
Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri, Max Schäfer
ICSE 2022 | May 2022
Software Engineering in Practice SEIP Track
TOGA: A Neural Method for Test Oracle Generation
Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu Lahiri
ICSE 2022 | May 2022
ICSE'22 ACM SIGSOFT Distinguished Award
SolType: Refinement Types for Solidity
Bryan Tan, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig, Yu Feng
POPL 2022 | January 2022
-
MergeBERT: Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Todd Mytkowicz, Negar Ghorbani, Sarah Fakhoury, Elizabeth Dinella, Christian Bird, Neel Sundaresan, Shuvendu Lahiri
August 2021
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis
Rangeet Pan, Vu Le, Nachi Nagappan, Sumit Gulwani, Shuvendu Lahiri, Mike Kaufman
2021 IEEE/ACM 43nd International Conference on Software Engineering (ICSE '21) | May 2021
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig
42nd IEEE Symposium on Security and Privacy | May 2021
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
May 2021
-
Demystifying Loops in Smart Contracts
Ben Mariano, Yanju Chen, Yu Feng, Shuvendu Lahiri, Isil Dillig
35th IEEE/ACM International Conference on Automated Software Engineering (ASE'20) | September 2020
A Dataset of Dockerfiles
Jordan Henkel, Shuvendu Lahiri, Christian Bird, Thomas Reps
ICSE 2020 | July 2020
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal
FMCAD | July 2020
Best paper award
Learning from, Understanding, and Supporting DevOps Artifacts for Docker
Jordan Henkel, Christian Bird, Shuvendu Lahiri, Thomas Reps
42nd International Conference on Software Engineering (ICSE'20) | May 2020
Towards Understanding and Fixing Upstream Merge Induced Conflicts in Divergent Forks: An Industrial Case Study
Chunhga Sung, Shuvendu Lahiri, Pallavi Choudhury, Mike Kaufman, Chao Wang
The 42nd International Conference on Software Engineering (ICSE SEIP Track), Seoul, Korea, May 2020 | May 2020
-
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, Kostas Ferles
Verified Software: Theories, Tools and Experiments | September 2019
Formal Specification and Verification of Smart Contracts for Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer
April 2019
-
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces
Jordan Henkel, Shuvendu Lahiri, Ben Liblit, Thomas Reps
Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’18) | November 2018
Verified Three-Way Program Merge
Marcelo Sousa, Isil Dillig, Shuvendu Lahiri
Object-Oriented Programming, Systems, Languages & Applications Conference (OOPSLA 2018) | November 2018
Datalog-based scalable semantic diffing of concurrent programs
Chungha Sung , Shuvendu Lahiri, Constantin Enea , Chao Wang
International Conference on Automated Software Engineering (ASE ’18) | September 2018
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu Lahiri, William Cook
Principles of Programming Languages 2018 (POPL 2018) | January 2018
-
Abstract Semantic Diffing of Evolving Concurrent Programs
Ahmed Bouajjani, Constantin Enea, Shuvendu Lahiri
Static Analysis Symposium 2017 (SAS'17) | August 2017
Static Assertion Checking of Production Software with Angelic Verification
| August 2017
Published by Microsoft
Refining Interprocedural Change-Impact Analysis using Equivalence Relations
Alex Gyori, Shuvendu Lahiri, Nimrod Partush
The International Symposium on Software Testing and Analysis 2017 (ISSTA '17) | July 2017
Optimizing Test Placement for Module-Level Regression Testing
August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Sophia Drossopoulou, Shuvendu Lahiri, Susan Eisenbach
European Symposium of Programming 2017 (ESOP'17) | April 2017
-
Wireless Protocol Validation Under Uncertainty
Jinghao Shi, Shuvendu Lahiri, Ranveer Chandra, Geoffrey Challen
Runtime Verification 2016 | July 2016
Runtime Verification 2016 Best Paper Award
-
Angelic Verification: Precise Verification Modulo Unknowns
Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das
Computer Aided Verification (CAV) | July 2015
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
Automated Differential Program Verification for Approximate Computing
| May 2015
Automated Differential Program Verification for Approximate Computing
Arvind Haran, Shaobo He, Zvonimir, Shuvendu Lahiri
May 2015
Helping developers help themselves: Automatic decomposition of code review changesets
Mike Barnett, Christian Bird, Shuvendu Lahiri, Joao Brunet
Proceedings of the 37th International Conference on Software Engineering | May 2015
-
Verification Modulo Versions: Towards Usable Verification
Francesco Logozzo, Shuvendu Lahiri
Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
Differential assertion checking
Kenneth McMillan, Rahul Sharma, Shuvendu Lahiri
ESEC/FSE 2013 | August 2013
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings
Sam Blackshear, Shuvendu Lahiri
Programming Language Design and Implementation (PLDI'13) | June 2013
Programming Language Design and Implementation (PLDI'13)
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
Towards practical reactive security audit using extended static checkers
Julien Vanegue, Shuvendu Lahiri
IEEE Symposium on Security and Privacy (Oakland'13) | May 2013
Differential Program Verification for Approximate Computing
| April 2013
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
-
Security audit using extended static checking: Is it cost-effective yet?
MSR-TR-2012-103 | October 2012
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
Computer-Aided Verification (CAV) | July 2012
Computer-Aided Verification (CAV)
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
MSR-TR-2012-9 | January 2012
Underspecified Harnesses and Interleaved Bugs
Saurabh Joshi, Shuvendu Lahiri, Akash Lal
Principles of Programming Languages (POPL) 2012 | January 2012
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-González
Static Analysis Symposium (SAS '11) | August 2011
Linear Maps
Shuvendu Lahiri, Shaz Qadeer, David Walker
ACM SIGPLAN Workshop on Programming Languages meets Program Verification | January 2011
Extended Princeton Technical Report TR-884-10, September 2010
-
Differential Static Analysis: Opportunities, Applications, and Challenges
Shuvendu Lahiri, Kapil Vaswani, Tony Hoare
2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) | November 2010
Conditional equivalence
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2010-119 | October 2010
ExplainHoudini: Making Houdini inference transparent
Shuvendu Lahiri, Julien Vanegue
MSR-TR-2010-118 | August 2010
12th International Conference on Verification, Model Checking, and Abstract Interpretation
Towards Scalable Modular Checking of User-Defined Properties
Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Julien Vanegue
Verified Software: Theories, Tools and Experiments (VSTTE 2010) | August 2010
An earlier version of this paper appeared as a Microsoft Research Technical Report MSR-TR-2008-82.
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-Gonzalez
MSR-TR-2010-11 | February 2010
Revised in October 2010
-
Call invariants
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2009-13 | July 2009
Complexity and algorithms for monomial and clausal predicate abstraction
Shuvendu Lahiri, Shaz Qadeer
International Conference on Automated Deduction (CADE '09) | March 2009
Intra-Module Inference
Shuvendu Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies
MSR-TR-2009-12 | February 2009
Computer Aided Verification (CAV '09)
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
Computer Aided Verification (CAV '09) | February 2009
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '09) | January 2009
Principles of Programming Languages (POPL '09)
-
Finding Errors in .NET with Feedback-Directed Random Testing
Carlos Pacheco, Shuvendu Lahiri, Thomas Ball
MSR-TR-2008-29 | July 2008
International Symposium on Software Testing and Analysis (ISSTA '08)
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2008-96 | July 2008
Towards Scalable Modular Checking of User-Defined Properties
Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Thomas Ball
MSR-TR-2008-82 | May 2008
Back to the Future: Revisiting Precise Program Verification using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL) | January 2008
-
Feedback-Directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
International Conference on Software Engineering (ICSE '07) | September 2007
Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic
Shuvendu Lahiri, Krishna Kumar Mehra
MSR-TR-2005-121 | September 2007
Proc. National Academy of Sciences
A Decision Procedure for Well-Founded Reachability
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2007-43 | April 2007
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
Logical Methods in Computer Science (LMCS '07) | January 2007
Predicate abstraction with indexed predicates
Shuvendu Lahiri, Randal E. Bryant
ACM Transactions on Computational Logic (TOCL '07) | January 2007
-
Feedback-directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
MSR-TR-2006-125 | September 2006
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, Vol 144: pp. 27-41
SMT Techniques for Fast Predicate Abstraction
Shuvendu Lahiri, Robert Nieuwenhuis, Albert Oliveras
Conference on Computer Aided Verification (CAV '06) | January 2006
ISBN: 3-540-37406-X
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
Verifying properties of well-founded linked lists
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '06) | January 2006
ISBN: 1-59593-027-2
-
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
Verifying Properties of Well-Founded Linked Lists
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2005-97 | July 2005
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
Predicate Abstraction via Symbolic Decison Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
MSR-TR-2005-53 | April 2005
Computer Aided Verification (CAV '05)
Publications by Research Area
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
October 2024
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
September 2024
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu Lahiri
The ACM International Conference on the Foundations of Software Engineering (FSE) | July 2024
GitHub page https://github.com/microsoft/nl-2-postcond/
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context
Lakshya A Agrawal, Aditya Kanade, Navin Goyal, Shuvendu Lahiri, Sriram Rajamani
NeurIPS 2023 | June 2023
Preprint
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
TOGA: A Neural Method for Test Oracle Generation
Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu Lahiri
ICSE 2022 | May 2022
ICSE'22 ACM SIGSOFT Distinguished Award
MergeBERT: Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Todd Mytkowicz, Negar Ghorbani, Sarah Fakhoury, Elizabeth Dinella, Christian Bird, Neel Sundaresan, Shuvendu Lahiri
August 2021
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
October 2024
Leveraging LLMs for Program Verification
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma
Formal Methods in Computer-Aided Design (FMCAD) | October 2024
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
September 2024
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu Lahiri
The ACM International Conference on the Foundations of Software Engineering (FSE) | July 2024
GitHub page https://github.com/microsoft/nl-2-postcond/
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
Formal Methods in Computer-Aided Design (FMCAD'24) | July 2024
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Shuvendu Lahiri
IEEE Transactions on Software Engineering | April 2024, Vol 50: pp. 2254-2268
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
Inference of Resource Management Specifications
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, Manu Sridharan
OOPSLA | October 2023
Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context
Lakshya A Agrawal, Aditya Kanade, Navin Goyal, Shuvendu Lahiri, Sriram Rajamani
NeurIPS 2023 | June 2023
Preprint
CODAMOSA: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models
Caroline Lemieux, Jeevana Priya Inala, Shuvendu Lahiri, Siddhartha Sen
ICSE'23 | May 2023
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Sarah Fakhoury, Negar Ghorbani, Todd Mytkowicz, Christian Bird, Jinu Jang, Neel Sundaresan, Shuvendu Lahiri, Elizabeth Dinella
The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '22) | November 2022
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
IEEE Transactions on Software Engineering (TSE'22) | July 2022
Using Pre-trained Language Models to Resolve Textual and Semantic Merge Conflicts (Experience Paper)
Jialu Zhang, Mike Kaufman, Todd Mytkowicz, Ruzica Piskac, Shuvendu Lahiri
ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis | July 2022
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript
Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri, Max Schäfer
ICSE 2022 | May 2022
Software Engineering in Practice SEIP Track
TOGA: A Neural Method for Test Oracle Generation
Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu Lahiri
ICSE 2022 | May 2022
ICSE'22 ACM SIGSOFT Distinguished Award
SolType: Refinement Types for Solidity
Bryan Tan, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig, Yu Feng
POPL 2022 | January 2022
MergeBERT: Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Todd Mytkowicz, Negar Ghorbani, Sarah Fakhoury, Elizabeth Dinella, Christian Bird, Neel Sundaresan, Shuvendu Lahiri
August 2021
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig
42nd IEEE Symposium on Security and Privacy | May 2021
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis
Rangeet Pan, Vu Le, Nachi Nagappan, Sumit Gulwani, Shuvendu Lahiri, Mike Kaufman
2021 IEEE/ACM 43nd International Conference on Software Engineering (ICSE '21) | May 2021
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
May 2021
Demystifying Loops in Smart Contracts
Ben Mariano, Yanju Chen, Yu Feng, Shuvendu Lahiri, Isil Dillig
35th IEEE/ACM International Conference on Automated Software Engineering (ASE'20) | September 2020
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal
FMCAD | July 2020
Best paper award
A Dataset of Dockerfiles
Jordan Henkel, Shuvendu Lahiri, Christian Bird, Thomas Reps
ICSE 2020 | July 2020
Towards Understanding and Fixing Upstream Merge Induced Conflicts in Divergent Forks: An Industrial Case Study
Chunhga Sung, Shuvendu Lahiri, Pallavi Choudhury, Mike Kaufman, Chao Wang
The 42nd International Conference on Software Engineering (ICSE SEIP Track), Seoul, Korea, May 2020 | May 2020
Learning from, Understanding, and Supporting DevOps Artifacts for Docker
Jordan Henkel, Christian Bird, Shuvendu Lahiri, Thomas Reps
42nd International Conference on Software Engineering (ICSE'20) | May 2020
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, Kostas Ferles
Verified Software: Theories, Tools and Experiments | September 2019
Formal Specification and Verification of Smart Contracts for Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer
April 2019
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces
Jordan Henkel, Shuvendu Lahiri, Ben Liblit, Thomas Reps
Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’18) | November 2018
Verified Three-Way Program Merge
Marcelo Sousa, Isil Dillig, Shuvendu Lahiri
Object-Oriented Programming, Systems, Languages & Applications Conference (OOPSLA 2018) | November 2018
Datalog-based scalable semantic diffing of concurrent programs
Chungha Sung , Shuvendu Lahiri, Constantin Enea , Chao Wang
International Conference on Automated Software Engineering (ASE ’18) | September 2018
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu Lahiri, William Cook
Principles of Programming Languages 2018 (POPL 2018) | January 2018
Abstract Semantic Diffing of Evolving Concurrent Programs
Ahmed Bouajjani, Constantin Enea, Shuvendu Lahiri
Static Analysis Symposium 2017 (SAS'17) | August 2017
Static Assertion Checking of Production Software with Angelic Verification
| August 2017
Published by Microsoft
Refining Interprocedural Change-Impact Analysis using Equivalence Relations
Alex Gyori, Shuvendu Lahiri, Nimrod Partush
The International Symposium on Software Testing and Analysis 2017 (ISSTA '17) | July 2017
Optimizing Test Placement for Module-Level Regression Testing
August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Sophia Drossopoulou, Shuvendu Lahiri, Susan Eisenbach
European Symposium of Programming 2017 (ESOP'17) | April 2017
Wireless Protocol Validation Under Uncertainty
Jinghao Shi, Shuvendu Lahiri, Ranveer Chandra, Geoffrey Challen
Runtime Verification 2016 | July 2016
Runtime Verification 2016 Best Paper Award
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
Angelic Verification: Precise Verification Modulo Unknowns
Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das
Computer Aided Verification (CAV) | July 2015
Automated Differential Program Verification for Approximate Computing
| May 2015
Automated Differential Program Verification for Approximate Computing
Arvind Haran, Shaobo He, Zvonimir, Shuvendu Lahiri
May 2015
Helping developers help themselves: Automatic decomposition of code review changesets
Mike Barnett, Christian Bird, Shuvendu Lahiri, Joao Brunet
Proceedings of the 37th International Conference on Software Engineering | May 2015
Verification Modulo Versions: Towards Usable Verification
Francesco Logozzo, Shuvendu Lahiri
Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
Differential assertion checking
Kenneth McMillan, Rahul Sharma, Shuvendu Lahiri
ESEC/FSE 2013 | August 2013
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings
Sam Blackshear, Shuvendu Lahiri
Programming Language Design and Implementation (PLDI'13) | June 2013
Programming Language Design and Implementation (PLDI'13)
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
Towards practical reactive security audit using extended static checkers
Julien Vanegue, Shuvendu Lahiri
IEEE Symposium on Security and Privacy (Oakland'13) | May 2013
Differential Program Verification for Approximate Computing
| April 2013
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
Security audit using extended static checking: Is it cost-effective yet?
MSR-TR-2012-103 | October 2012
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
Computer-Aided Verification (CAV) | July 2012
Computer-Aided Verification (CAV)
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
Underspecified Harnesses and Interleaved Bugs
Saurabh Joshi, Shuvendu Lahiri, Akash Lal
Principles of Programming Languages (POPL) 2012 | January 2012
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
MSR-TR-2012-9 | January 2012
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-González
Static Analysis Symposium (SAS '11) | August 2011
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
Differential Static Analysis: Opportunities, Applications, and Challenges
Shuvendu Lahiri, Kapil Vaswani, Tony Hoare
2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) | November 2010
Conditional equivalence
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2010-119 | October 2010
ExplainHoudini: Making Houdini inference transparent
Shuvendu Lahiri, Julien Vanegue
MSR-TR-2010-118 | August 2010
12th International Conference on Verification, Model Checking, and Abstract Interpretation
Towards Scalable Modular Checking of User-Defined Properties
Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Julien Vanegue
Verified Software: Theories, Tools and Experiments (VSTTE 2010) | August 2010
An earlier version of this paper appeared as a Microsoft Research Technical Report MSR-TR-2008-82.
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-Gonzalez
MSR-TR-2010-11 | February 2010
Revised in October 2010
Call invariants
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2009-13 | July 2009
Complexity and algorithms for monomial and clausal predicate abstraction
Shuvendu Lahiri, Shaz Qadeer
International Conference on Automated Deduction (CADE '09) | March 2009
Intra-Module Inference
Shuvendu Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies
MSR-TR-2009-12 | February 2009
Computer Aided Verification (CAV '09)
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
Computer Aided Verification (CAV '09) | February 2009
Finding Errors in .NET with Feedback-Directed Random Testing
Carlos Pacheco, Shuvendu Lahiri, Thomas Ball
MSR-TR-2008-29 | July 2008
International Symposium on Software Testing and Analysis (ISSTA '08)
Towards Scalable Modular Checking of User-Defined Properties
Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Thomas Ball
MSR-TR-2008-82 | May 2008
Predicate abstraction with indexed predicates
Shuvendu Lahiri, Randal E. Bryant
ACM Transactions on Computational Logic (TOCL '07) | January 2007
SMT Techniques for Fast Predicate Abstraction
Shuvendu Lahiri, Robert Nieuwenhuis, Albert Oliveras
Conference on Computer Aided Verification (CAV '06) | January 2006
ISBN: 3-540-37406-X
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
-
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
October 2024
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
September 2024
Wireless Protocol Validation Under Uncertainty
Jinghao Shi, Shuvendu Lahiri, Ranveer Chandra, Geoffrey Challen
Runtime Verification 2016 | July 2016
Runtime Verification 2016 Best Paper Award
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
Computer-Aided Verification (CAV) | July 2012
Computer-Aided Verification (CAV)
Back to the Future: Revisiting Precise Program Verification using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL) | January 2008
Feedback-Directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
International Conference on Software Engineering (ICSE '07) | September 2007
A Decision Procedure for Well-Founded Reachability
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2007-43 | April 2007
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
Logical Methods in Computer Science (LMCS '07) | January 2007
Feedback-directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
MSR-TR-2006-125 | September 2006
Predicate Abstraction via Symbolic Decison Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
MSR-TR-2005-53 | April 2005
Computer Aided Verification (CAV '05)
-
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript
Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri, Max Schäfer
ICSE 2022 | May 2022
Software Engineering in Practice SEIP Track
Towards practical reactive security audit using extended static checkers
Julien Vanegue, Shuvendu Lahiri
IEEE Symposium on Security and Privacy (Oakland'13) | May 2013
-
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
-
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '09) | January 2009
Principles of Programming Languages (POPL '09)
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2008-96 | July 2008
Verifying properties of well-founded linked lists
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '06) | January 2006
ISBN: 1-59593-027-2
Verifying Properties of Well-Founded Linked Lists
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2005-97 | July 2005
-
Linear Maps
Shuvendu Lahiri, Shaz Qadeer, David Walker
ACM SIGPLAN Workshop on Programming Languages meets Program Verification | January 2011
Extended Princeton Technical Report TR-884-10, September 2010
-
Complexity and algorithms for monomial and clausal predicate abstraction
Shuvendu Lahiri, Shaz Qadeer
International Conference on Automated Deduction (CADE '09) | March 2009
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, Vol 144: pp. 27-41
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
-
Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic
Shuvendu Lahiri, Krishna Kumar Mehra
MSR-TR-2005-121 | September 2007
Proc. National Academy of Sciences
Publications by Type
-
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, Lidong Zhou
October 2024
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jay Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
September 2024
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Piali Choudhury, Curtis von Veh, Madan Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao
August 2022
-
LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Shuvendu Lahiri
IEEE Transactions on Software Engineering | April 2024, Vol 50: pp. 2254-2268
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
IEEE Transactions on Software Engineering (TSE'22) | July 2022
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madanlal Musuvathi, Madan Musuvathi
Electr. Notes Theor. Comput. Sci. | January 2006, Vol 144: pp. 27-41
-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu Lahiri, Tahina Ramananandro, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy
2025 International Conference on Software Engineering | April 2025
Leveraging LLMs for Program Verification
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma
Formal Methods in Computer-Aided Design (FMCAD) | October 2024
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu Lahiri
The ACM International Conference on the Foundations of Software Engineering (FSE) | July 2024
GitHub page https://github.com/microsoft/nl-2-postcond/
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
Formal Methods in Computer-Aided Design (FMCAD'24) | July 2024
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu Lahiri
2024 International Conference on Software Engineering | May 2024
Poster track
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Madan Musuvathi, Akash Lal, Aseem Rastogi, Nikhil Swamy, Rahul Sharma
2023 Empirical Methods in Natural Language Processing | December 2023
EMNLP-Findings 2023
Inference of Resource Management Specifications
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, Manu Sridharan
OOPSLA | October 2023
Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context
Lakshya A Agrawal, Aditya Kanade, Navin Goyal, Shuvendu Lahiri, Sriram Rajamani
NeurIPS 2023 | June 2023
Preprint
CODAMOSA: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models
Caroline Lemieux, Jeevana Priya Inala, Shuvendu Lahiri, Siddhartha Sen
ICSE'23 | May 2023
Fault-Aware Neural Code Rankers
Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andres Codas, Mark Encarnación, Shuvendu Lahiri, Madan Musuvathi, Jianfeng Gao
NeurIPS 2022 | November 2022
Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Sarah Fakhoury, Negar Ghorbani, Todd Mytkowicz, Christian Bird, Jinu Jang, Neel Sundaresan, Shuvendu Lahiri, Elizabeth Dinella
The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '22) | November 2022
Using Pre-trained Language Models to Resolve Textual and Semantic Merge Conflicts (Experience Paper)
Jialu Zhang, Mike Kaufman, Todd Mytkowicz, Ruzica Piskac, Shuvendu Lahiri
ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis | July 2022
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript
Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri, Max Schäfer
ICSE 2022 | May 2022
Software Engineering in Practice SEIP Track
TOGA: A Neural Method for Test Oracle Generation
Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu Lahiri
ICSE 2022 | May 2022
ICSE'22 ACM SIGSOFT Distinguished Award
SolType: Refinement Types for Solidity
Bryan Tan, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig, Yu Feng
POPL 2022 | January 2022
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts
Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, Isil Dillig
42nd IEEE Symposium on Security and Privacy | May 2021
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis
Rangeet Pan, Vu Le, Nachi Nagappan, Sumit Gulwani, Shuvendu Lahiri, Mike Kaufman
2021 IEEE/ACM 43nd International Conference on Software Engineering (ICSE '21) | May 2021
Demystifying Loops in Smart Contracts
Ben Mariano, Yanju Chen, Yu Feng, Shuvendu Lahiri, Isil Dillig
35th IEEE/ACM International Conference on Automated Software Engineering (ASE'20) | September 2020
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost
Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal
FMCAD | July 2020
Best paper award
A Dataset of Dockerfiles
Jordan Henkel, Shuvendu Lahiri, Christian Bird, Thomas Reps
ICSE 2020 | July 2020
Towards Understanding and Fixing Upstream Merge Induced Conflicts in Divergent Forks: An Industrial Case Study
Chunhga Sung, Shuvendu Lahiri, Pallavi Choudhury, Mike Kaufman, Chao Wang
The 42nd International Conference on Software Engineering (ICSE SEIP Track), Seoul, Korea, May 2020 | May 2020
Learning from, Understanding, and Supporting DevOps Artifacts for Docker
Jordan Henkel, Christian Bird, Shuvendu Lahiri, Thomas Reps
42nd International Conference on Software Engineering (ICSE'20) | May 2020
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, Kostas Ferles
Verified Software: Theories, Tools and Experiments | September 2019
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces
Jordan Henkel, Shuvendu Lahiri, Ben Liblit, Thomas Reps
Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’18) | November 2018
Verified Three-Way Program Merge
Marcelo Sousa, Isil Dillig, Shuvendu Lahiri
Object-Oriented Programming, Systems, Languages & Applications Conference (OOPSLA 2018) | November 2018
Datalog-based scalable semantic diffing of concurrent programs
Chungha Sung , Shuvendu Lahiri, Constantin Enea , Chao Wang
International Conference on Automated Software Engineering (ASE ’18) | September 2018
Verifying Equivalence of Database-Driven Applications
Yuepeng Wang, Isil Dillig, Shuvendu Lahiri, William Cook
Principles of Programming Languages 2018 (POPL 2018) | January 2018
Abstract Semantic Diffing of Evolving Concurrent Programs
Ahmed Bouajjani, Constantin Enea, Shuvendu Lahiri
Static Analysis Symposium 2017 (SAS'17) | August 2017
Refining Interprocedural Change-Impact Analysis using Equivalence Relations
Alex Gyori, Shuvendu Lahiri, Nimrod Partush
The International Symposium on Software Testing and Analysis 2017 (ISSTA '17) | July 2017
Optimizing Test Placement for Module-Level Regression Testing
August Shi, Suresh Thummalapenta, Shuvendu Lahiri, Nikolaj Bjørner, Jacek Czerwonka
Proceedings of the 39th International Conference on Software Engineering (ICSE'17) | May 2017
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Sophia Drossopoulou, Shuvendu Lahiri, Susan Eisenbach
European Symposium of Programming 2017 (ESOP'17) | April 2017
Wireless Protocol Validation Under Uncertainty
Jinghao Shi, Shuvendu Lahiri, Ranveer Chandra, Geoffrey Challen
Runtime Verification 2016 | July 2016
Runtime Verification 2016 Best Paper Award
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
Computer Aided Verification (CAV'15) | July 2015
Computer Aided Verification (CAV'15)
Angelic Verification: Precise Verification Modulo Unknowns
Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das
Computer Aided Verification (CAV) | July 2015
Automated Differential Program Verification for Approximate Computing
Arvind Haran, Shaobo He, Zvonimir, Shuvendu Lahiri
May 2015
Helping developers help themselves: Automatic decomposition of code review changesets
Mike Barnett, Christian Bird, Shuvendu Lahiri, Joao Brunet
Proceedings of the 37th International Conference on Software Engineering | May 2015
Verification Modulo Versions: Towards Usable Verification
Francesco Logozzo, Shuvendu Lahiri
Proceedings of the 35th conference on Programming Languages, Design, and Implementation (PLDI 2014) | June 2014
Differential assertion checking
Kenneth McMillan, Rahul Sharma, Shuvendu Lahiri
ESEC/FSE 2013 | August 2013
Will You Still Compile Me Tomorrow? Static Cross-Version Compiler Validation
Chris Hawblitzel, Shuvendu Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
Foundations of Software Engineering (FSE'13) | August 2013
Differential Assertion Checking
Shuvendu Lahiri, Ken McMillan, Chris Hawblitzel, Kenneth McMillan
Foundations of Software Engineering (FSE'13) | August 2013
Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings
Sam Blackshear, Shuvendu Lahiri
Programming Language Design and Implementation (PLDI'13) | June 2013
Programming Language Design and Implementation (PLDI'13)
Towards Modularly Comparing Programs using Automated Theorem Provers
Chris Hawblitzel, Shuvendu Lahiri, Ming Kawaguchi, Henrique Rebelo
International Conference on Automated Deduction (CADE '13) | June 2013
International Conference on Automated Deduction (CADE '13)
Towards practical reactive security audit using extended static checkers
Julien Vanegue, Shuvendu Lahiri
IEEE Symposium on Security and Privacy (Oakland'13) | May 2013
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
Computer-Aided Verification (CAV) | July 2012
Computer-Aided Verification (CAV)
SymDiff: A language-agnostic semantic diff tool for imperative programs
Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebelo
Computer Aided Verification (CAV '12) (Tool description) | July 2012
Underspecified Harnesses and Interleaved Bugs
Saurabh Joshi, Shuvendu Lahiri, Akash Lal
Principles of Programming Languages (POPL) 2012 | January 2012
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-González
Static Analysis Symposium (SAS '11) | August 2011
Linear Maps
Shuvendu Lahiri, Shaz Qadeer, David Walker
ACM SIGPLAN Workshop on Programming Languages meets Program Verification | January 2011
Extended Princeton Technical Report TR-884-10, September 2010
Differential Static Analysis: Opportunities, Applications, and Challenges
Shuvendu Lahiri, Kapil Vaswani, Tony Hoare
2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) | November 2010
Towards Scalable Modular Checking of User-Defined Properties
Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Julien Vanegue
Verified Software: Theories, Tools and Experiments (VSTTE 2010) | August 2010
An earlier version of this paper appeared as a Microsoft Research Technical Report MSR-TR-2008-82.
Complexity and algorithms for monomial and clausal predicate abstraction
Shuvendu Lahiri, Shaz Qadeer
International Conference on Automated Deduction (CADE '09) | March 2009
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
Computer Aided Verification (CAV '09) | February 2009
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '09) | January 2009
Principles of Programming Languages (POPL '09)
Back to the Future: Revisiting Precise Program Verification using SMT Solvers
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL) | January 2008
Feedback-Directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
International Conference on Software Engineering (ICSE '07) | September 2007
Predicate abstraction with indexed predicates
Shuvendu Lahiri, Randal E. Bryant
ACM Transactions on Computational Logic (TOCL '07) | January 2007
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
Logical Methods in Computer Science (LMCS '07) | January 2007
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
Automated Reasoning, Third International Joint Conference (IJCAR '06) | January 2006
ISBN: 3-540-37187-7
Verifying properties of well-founded linked lists
Shuvendu Lahiri, Shaz Qadeer
Principles of Programming Languages (POPL '06) | January 2006
ISBN: 1-59593-027-2
SMT Techniques for Fast Predicate Abstraction
Shuvendu Lahiri, Robert Nieuwenhuis, Albert Oliveras
Conference on Computer Aided Verification (CAV '06) | January 2006
ISBN: 3-540-37406-X
-
MergeBERT: Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Todd Mytkowicz, Negar Ghorbani, Sarah Fakhoury, Elizabeth Dinella, Christian Bird, Neel Sundaresan, Shuvendu Lahiri
August 2021
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu Lahiri
May 2021
Formal Specification and Verification of Smart Contracts for Azure Blockchain
Yuepeng Wang, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer
April 2019
-
Static Assertion Checking of Production Software with Angelic Verification
| August 2017
Published by Microsoft
Automated Differential Program Verification for Approximate Computing
| May 2015
Automatic Rootcausing for Program Equivalence Failures in Binaries
Shuvendu Lahiri, Rohit Sinha, Chris Hawblitzel
MSR-TR-2014-11 | February 2014
Differential Program Verification for Approximate Computing
| April 2013
Differential Assertion Checking
Shuvendu Lahiri, Kenneth McMillan, Chris Hawblitzel
MSR-TR-2013-34 | March 2013
Security audit using extended static checking: Is it cost-effective yet?
MSR-TR-2012-103 | October 2012
Corral: A Solver for Reachability Modulo Theories
Akash Lal, Shaz Qadeer, Shuvendu Lahiri
MSR-TR-2012-9 | January 2012
Towards Modularly Comparing Programs using Automated Theorem Provers
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo, Chris Hawblitzel
MSR-TR-2011-112 | October 2011
The set of benchmarks used in this paper, along with the proof (in text format).
Mutual Summaries: Unifying Program Comparison Techniques
Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2011-78 | August 2011
Informal proceedings of BOOGIE 2011 workshop
Conditional equivalence
Ming Kawaguchi, Shuvendu Lahiri, Henrique Rebelo
MSR-TR-2010-119 | October 2010
ExplainHoudini: Making Houdini inference transparent
Shuvendu Lahiri, Julien Vanegue
MSR-TR-2010-118 | August 2010
12th International Conference on Verification, Model Checking, and Abstract Interpretation
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Patrice Godefroid, Shuvendu Lahiri, Cindy Rubio-Gonzalez
MSR-TR-2010-11 | February 2010
Revised in October 2010
Call invariants
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2009-13 | July 2009
Intra-Module Inference
Shuvendu Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies
MSR-TR-2009-12 | February 2009
Computer Aided Verification (CAV '09)
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2008-96 | July 2008
Finding Errors in .NET with Feedback-Directed Random Testing
Carlos Pacheco, Shuvendu Lahiri, Thomas Ball
MSR-TR-2008-29 | July 2008
International Symposium on Software Testing and Analysis (ISSTA '08)
Towards Scalable Modular Checking of User-Defined Properties
Brian Hackett, Shuvendu Lahiri, Shaz Qadeer, Thomas Ball
MSR-TR-2008-82 | May 2008
Interpolant based Decision Procedure for Quantifier-free Presburger Arithmetic
Shuvendu Lahiri, Krishna Kumar Mehra
MSR-TR-2005-121 | September 2007
Proc. National Academy of Sciences
A Decision Procedure for Well-Founded Reachability
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2007-43 | April 2007
Feedback-directed Random Test Generation
Carlos Pacheco, Shuvendu Lahiri, Michael D. Ernst, Thomas Ball
MSR-TR-2006-125 | September 2006
Solving Sparse Linear Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2006-47 | April 2006
Zap: Automated Theorem Proving for Software Analysis
Thomas Ball, Shuvendu Lahiri, Madanlal Musuvathi, Thomas Ball, Madan Musuvathi
MSR-TR-2005-137 | October 2005
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
Verifying Properties of Well-Founded Linked Lists
Shuvendu Lahiri, Shaz Qadeer
MSR-TR-2005-97 | July 2005
An Efficient Decision Procedure for UTVPI Constraints
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-67 | May 2005
Frontiers of Combining Systems (FroCos '05)
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals
Shuvendu Lahiri, Madan Musuvathi
MSR-TR-2005-61 | May 2005
Predicate Abstraction via Symbolic Decison Procedures
Shuvendu Lahiri, Thomas Ball, Byron Cook
MSR-TR-2005-53 | April 2005
Computer Aided Verification (CAV '05)