| 2026 | TACAS | VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. | Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett |
| 2025 | CGO | LLM-Vectorizer: LLM-Based Verified Loop Vectorizer. | Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, Shuvendu K. Lahiri |
| 2025 | ICLR | 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 K. Lahiri, Tao Xie, Lidong Zhou |
| 2025 | ICSE | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. | Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, Nikhil Swamy |
| 2025 | ICSE | 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. | Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy |
| 2024 | FMCAD | Leveraging LLMs for Program Verification. | Adharsh Kamath, J. Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma |
| 2024 | FMCAD | Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. | Shuvendu K. Lahiri |
| 2024 | ICSE | NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions. | Sarah Fakhoury, Saikat Chakraborty, Madanlal Musuvathi, Shuvendu K. Lahiri |
| 2024 | ICSE | Exploring the Effectiveness of LLM based Test-driven Interactive Code Generation: User Study and Empirical Evaluation. | Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Madan Musuvathi, Shuvendu K. Lahiri |
| 2023 | EMNLP | Ranking LLM-Generated Loop Invariants for Program Verification. | Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy |
| 2023 | ICSE | CodaMosa: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models. | Caroline Lemieux, Jeevana Priya Inala, Shuvendu K. Lahiri, Siddhartha Sen |
| 2022 | ICSE | TOGA: A Neural Method for Test Oracle Generation. | Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu K. Lahiri |
| 2022 | ICSE | InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript. | Saikat Dutta, Diego Garbervetsky, Shuvendu K. Lahiri, Max Schfer |
| 2022 | ISSTA | Using pre-trained language models to resolve textual and semantic merge conflicts (experience paper). | Jialu Zhang, Todd Mytkowicz, Mike Kaufman, Ruzica Piskac, Shuvendu K. Lahiri |
| 2022 | SAS | Automated Synthesis of Asynchronizations. | Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2021 | ICSE | Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis. | Rangeet Pan, Vu Le, Nachiappan Nagappan, Sumit Gulwani, Shuvendu K. Lahiri, Mike Kaufman |
| 2021 | SP | SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. | Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig |
| 2020 | FMCAD | Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. | Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal |
| 2020 | ICSE | Learning from, understanding, and supporting DevOps artifacts for docker. | Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps |
| 2020 | ICSE | Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. | Chungha Sung, Shuvendu K. Lahiri, Mike Kaufman, Pallavi Choudhury, Chao Wang |
| 2020 | ICSE | Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. | Chungha Sung, Shuvendu K. Lahiri, Mike Kaufman, Pallavi Choudhury, Jessica Wolk, Chao Wang |
| 2020 | MSR | A Dataset of Dockerfiles. | Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps |
| 2017 | ESOP | Modular Verification of Procedure Equivalence in the Presence of Memory Allocation. | Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, Susan Eisenbach |
| 2017 | ICSE | Optimizing test placement for module-level regression testing. | August Shi, Suresh Thummalapenta, Shuvendu K. Lahiri, Nikolaj S. Bjrner, Jacek Czerwonka |
| 2017 | ISSTA | Refining interprocedural change-impact analysis using equivalence relations. | Alex Gyori, Shuvendu K. Lahiri, Nimrod Partush |
| 2017 | SAS | Abstract Semantic Diffing of Evolving Concurrent Programs. | Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2016 | RV | Wireless Protocol Validation Under Uncertainty. | Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, Geoffrey Challen |
| 2015 | CAV | Angelic Verification: Precise Verification Modulo Unknowns. | Ankush Das, Shuvendu K. Lahiri, Akash Lal, Yi Li |
| 2015 | CAV | Automatic Rootcausing for Program Equivalence Failures in Binaries. | Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel |
| 2015 | ICSE | Helping Developers Help Themselves: Automatic Decomposition of Code Review Changesets. | Mike Barnett, Christian Bird, Joo Brunet, Shuvendu K. Lahiri |
| 2014 | PLDI | Verification modulo versions: towards usable verification. | Francesco Logozzo, Shuvendu K. Lahiri, Manuel Fhndrich, Sam Blackshear |
| 2013 | CADE | Towards Modularly Comparing Programs Using Automated Theorem Provers. | Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Reblo |
| 2013 | PLDI | Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. | Sam Blackshear, Shuvendu K. Lahiri |
| 2013 | SP | Towards Practical Reactive Security Audit Using Extended Static Checkers. | Julien Vanegue, Shuvendu K. Lahiri |
| 2012 | CAV | SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. | Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Reblo |
| 2012 | CAV | A Solver for Reachability Modulo Theories. | Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri |
| 2012 | POPL | Underspecified harnesses and interleaved bugs. | Saurabh Joshi, Shuvendu K. Lahiri, Akash Lal |
| 2011 | CAV | SMT-Based Modular Analysis of Sequential Systems Code. | Shuvendu K. Lahiri |
| 2011 | SAS | Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation. | Patrice Godefroid, Shuvendu K. Lahiri, Cindy Rubio-Gonzlez |
| 2011 | VMCAI | ExplainHoudini: Making Houdini Inference Transparent. | Shuvendu K. Lahiri, Julien Vanegue |
| 2010 | VMCAI | Abstract Threads. | Shuvendu K. Lahiri, Alexander Malkis, Shaz Qadeer |
| 2009 | CADE | Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2009 | CAV | Intra-module Inference. | Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies |
| 2009 | CAV | Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. | Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
| 2009 | POPL | Unifying type checking and property checking for low-level code. | Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer |
| 2008 | ICCAD | Embedded software verification: challenges and solutions. | Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening |
| 2008 | ISSTA | Finding errors in .net with feedback-directed random testing. | Carlos Pacheco, Shuvendu K. Lahiri, Thomas Ball |
| 2008 | POPL | Back to the future: revisiting precise program verification using SMT solvers. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2007 | ICSE | Feedback-Directed Random Test Generation. | Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, Thomas Ball |
| 2007 | TACAS | A Reachability Predicate for Analyzing Low-Level Software. | Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
| 2006 | CADE | Solving Sparse Linear Constraints. | Shuvendu K. Lahiri, Madanlal Musuvathi |
| 2006 | CAV | SMT Techniques for Fast Predicate Abstraction. | Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras |
| 2006 | POPL | Verifying properties of well-founded linked lists. | Shuvendu K. Lahiri, Shaz Qadeer |
| 2005 | CAV | Predicate Abstraction via Symbolic Decision Procedures. | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
| 2005 | LPAR | Zap: Automated Theorem Proving for Software Analysis. | Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi |
| 2004 | CAV | Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. | Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang |
| 2004 | CAV | Indexed Predicate Discovery for Unbounded System Verification. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2004 | CAV | The UCLID Decision Procedure. | Shuvendu K. Lahiri, Sanjit A. Seshia |
| 2004 | TACAS | Revisiting Positive Equality. | Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur |
| 2004 | VMCAI | Constructing Quantified Invariants via Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | CAV | Deductive Verification of Advanced Out-of-Order Microprocessors. | Shuvendu K. Lahiri, Randal E. Bryant |
| 2003 | CAV | A Symbolic Approach to Predicate Abstraction. | Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook |
| 2003 | DAC | A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. | Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant |
| 2002 | CAV | Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |
| 2002 | FMCAD | Modeling and Verification of Out-of-Order Microprocessors in UCLID. | Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant |
| 1999 | VLSID | Controlling State Explosion in Static Simulation by Selective Composition. | Partha Pratim Chakrabarti, Pallab Dasgupta, Partha Pratim Das, Arnob Roy, Shuvendu K. Lahiri, Mrinal Bose |