default search action
Shuvendu K. Lahiri
Person information
- affiliation: Microsoft Research, Redmond, WA, USA
- affiliation (PhD): Carnegie Mellon University, Pittsburgh, PA, USA
- affiliation: Indian Institute of Technology, Kharagpur, India
- not to be confused with: S. K. Lahiri 0001
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j14]Madeline Endres
, Sarah Fakhoury
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proc. ACM Softw. Eng. 1(FSE): 1889-1912 (2024) - [j13]Sarah Fakhoury
LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation. IEEE Trans. Software Eng. 50(9): 2254-2268 (2024) - [c80]Shuvendu K. Lahiri
AI-Assisted User Intent Formalization for Programs: Problem and Applications (Invited Talk). AIware 2024 - [c79]Sarah Fakhoury
Exploring the Effectiveness of LLM based Test-driven Interactive Code Generation: User Study and Empirical Evaluation. ICSE Companion 2024: 390-391 - [c78]Sarah Fakhoury
NL2Fix: Generating Functionally Correct Code Edits from Bug Descriptions. ICSE Companion 2024: 410-411 - [c77]Elizabeth Dinella
Inferring Natural Preconditions via Program Transformation. SIGSOFT FSE Companion 2024: 657-658 - [i38]Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Shuvendu K. Lahiri:
LLM-based Test-driven Interactive Code Generation: User Study and Empirical Evaluation. CoRR abs/2404.10100 (2024) - [i37]Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy:
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. CoRR abs/2404.10362 (2024) - [i36]Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, Nikhil Swamy:
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. CoRR abs/2405.01787 (2024) - [i35]Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, Shuvendu K. Lahiri:
LLM-Vectorizer: LLM-based Verified Loop Vectorizer. CoRR abs/2406.04693 (2024) - [i34]Shuvendu K. Lahiri:
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. CoRR abs/2406.09757 (2024) - [i33]Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu:
AutoVerus: Automated Proof Generation for Rust Code. CoRR abs/2409.13082 (2024) - [i32]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:
Automated Proof Generation for Rust Code via Self-Evolution. CoRR abs/2410.15756 (2024) - 2023
- [j12]Narges Shadab
Inference of Resource Management Specifications. Proc. ACM Program. Lang. 7(OOPSLA2): 1705-1728 (2023) - [j11]Elizabeth Dinella
DeepMerge: Learning to Merge Programs. IEEE Trans. Software Eng. 49(4): 1599-1614 (2023) - [c76]Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy:
Ranking LLM-Generated Loop Invariants for Program Verification. EMNLP (Findings) 2023: 9164-9175 - [c75]Caroline Lemieux, Jeevana Priya Inala, Shuvendu K. Lahiri, Siddhartha Sen:
CodaMosa: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models. ICSE 2023: 919-931 - [c74]Lakshya A. Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K. Lahiri, Sriram K. Rajamani:
Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context. NeurIPS 2023 - [i31]Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi, Shuvendu K. Lahiri:
Towards Generating Functionally Correct Code Edits from Natural Language Issue Descriptions. CoRR abs/2304.03816 (2023) - [i30]Lakshya A. Agrawal
Guiding Language Models of Code with Global Context using Monitors. CoRR abs/2306.10763 (2023) - [i29]Narges Shadab, Pritam M. Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, Manu Sridharan:
Automatic Inference of Resource Leak Specifications. CoRR abs/2306.11953 (2023) - [i28]Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri:
Formalizing Natural Language Intent into Program Specifications via Large Language Models. CoRR abs/2310.01831 (2023) - [i27]Elizabeth Dinella, Shuvendu K. Lahiri, Mayur Naik:
Program Structure Aware Precondition Generation. CoRR abs/2310.02154 (2023) - [i26]Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy:
Ranking LLM-Generated Loop Invariants for Program Verification. CoRR abs/2310.09342 (2023) - [i25]Adharsh Kamath
Finding Inductive Loop Invariants using Large Language Models. CoRR abs/2311.07948 (2023) - [i24]Pritam M. Gharat, Narges Shadab, Shrey Tiwari, Shuvendu K. Lahiri, Akash Lal:
Resource Leak Checker (RLC#) for C# Code using CodeQL. CoRR abs/2312.01912 (2023) - 2022
- [j10]Bryan Tan
SolType: refinement types for arithmetic overflow in solidity. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) - [c73]Saikat Dutta, Diego Garbervetsky, Shuvendu K. Lahiri, Max Schäfer:
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript. ICSE (SEIP) 2022: 165-174 - [c72]Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, Shuvendu K. Lahiri:
TOGA: A Neural Method for Test Oracle Generation. ICSE 2022: 2130-2141 - [c71]Jialu Zhang, Todd Mytkowicz, Mike Kaufman, Ruzica Piskac
Using pre-trained language models to resolve textual and semantic merge conflicts (experience paper). ISSTA 2022: 77-88 - [c70]Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andrés Codas, Mark Encarnación, Shuvendu K. Lahiri, Madanlal Musuvathi, Jianfeng Gao:
Fault-Aware Neural Code Rankers. NeurIPS 2022 - [c69]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Automated Synthesis of Asynchronizations. SAS 2022: 135-159 - [c68]Alexey Svyatkovskiy, Sarah Fakhoury, Negar Ghorbani, Todd Mytkowicz, Elizabeth Dinella, Christian Bird, Jinu Jang, Neel Sundaresan, Shuvendu K. Lahiri:
Program merge conflict resolution via neural transformers. ESEC/SIGSOFT FSE 2022: 822-833 - [i23]Jeevana Priya Inala, Chenglong Wang, Mei Yang, Andrés Codas, Mark Encarnación, Shuvendu K. Lahiri, Madanlal Musuvathi, Jianfeng Gao:
Fault-Aware Neural Code Rankers. CoRR abs/2206.03865 (2022) - [i22]Shuvendu K. Lahiri, Aaditya Naik, Georgios Sakkas, Piali Choudhury, Curtis von Veh, Madanlal Musuvathi, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao:
Interactive Code Generation via Test-Driven User-Intent Formalization. CoRR abs/2208.05950 (2022) - [i21]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Automated Synthesis of Asynchronizations. CoRR abs/2209.06648 (2022) - 2021
- [c67]Rangeet Pan, Vu Le, Nachiappan Nagappan, Sumit Gulwani, Shuvendu K. Lahiri, Mike Kaufman:
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis. ICSE 2021: 785-796 - [c66]Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig:
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. SP 2021: 555-571 - [i20]Rangeet Pan, Vu Le, Nachiappan Nagappan, Sumit Gulwani, Shuvendu K. Lahiri, Mike Kaufman:
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis. CoRR abs/2103.02004 (2021) - [i19]Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy, Christian Bird, Mayur Naik, Shuvendu K. Lahiri:
DeepMerge: Learning to Merge Programs. CoRR abs/2105.07569 (2021) - [i18]Alexey Svyatkovskiy, Todd Mytkowicz, Negar Ghorbani, Sarah Fakhoury, Elizabeth Dinella, Christian Bird, Neel Sundaresan, Shuvendu K. Lahiri:
MergeBERT: Program Merge Conflict Resolution via Neural Transformers. CoRR abs/2109.00084 (2021) - [i17]Elizabeth Dinella, Shuvendu K. Lahiri, Todd Mytkowicz, Gabriel Ryan:
Neural Unit Test Suggestions. CoRR abs/2109.09262 (2021) - [i16]Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, Yu Feng:
SolType: Refinement Types for Solidity. CoRR abs/2110.00677 (2021) - [i15]Saikat Dutta, Diego Garbervetsky, Shuvendu K. Lahiri, Max Schäfer:
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript. CoRR abs/2111.09625 (2021) - [i14]Jialu Zhang, Todd Mytkowicz, Mike Kaufman, Ruzica Piskac, Shuvendu K. Lahiri:
Can Pre-trained Language Models be Used to Resolve Textual and Semantic Merge Conflicts? CoRR abs/2111.11904 (2021) - 2020
- [c65]Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal:
Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. FMCAD 2020: 169-178 - [c64]Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps:
Learning from, understanding, and supporting DevOps artifacts for docker. ICSE 2020: 38-49 - [c63]Chungha Sung
Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. ICSE (SEIP) 2020: 172-181 - [c62]Chungha Sung
Towards understanding and fixing upstream merge induced conflicts in divergent forks: an industrial case study. ICSE (Companion Volume) 2020: 320-321 - [c61]Benjamin Mariano, Yanju Chen, Yu Feng, Shuvendu K. Lahiri, Isil Dillig:
Demystifying Loops in Smart Contracts. ASE 2020: 262-274 - [c60]Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps:
A Dataset of Dockerfiles. MSR 2020: 528-532 - [e4]Shuvendu K. Lahiri, Chao Wang:
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science 12224, Springer 2020, ISBN 978-3-030-53287-1 [contents] - [e3]Shuvendu K. Lahiri, Chao Wang:
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science 12225, Springer 2020, ISBN 978-3-030-53290-1 [contents] - [d4]Jordan Henkel
ICSE 2020 Artifact for: Learning from, Understanding, and Supporting DevOps Artifacts for Docker. Zenodo, 2020 - [i13]Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps:
Learning from, Understanding, and Supporting DevOps Artifacts for Docker. CoRR abs/2002.03064 (2020) - [i12]Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps:
A Dataset of Dockerfiles. CoRR abs/2003.12912 (2020)
2010 – 2019
- 2019
- [j9]Ahmed Bouajjani, Constantin Enea
Abstract semantic diffing of evolving concurrent programs. Formal Methods Syst. Des. 54(1): 4-26 (2019) - [c59]Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer, Kostas Ferles:
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. VSTTE 2019: 87-106 - [i11]Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit, Thomas W. Reps:
Enabling Open-World Specification Mining via Unsupervised Learning. CoRR abs/1904.12098 (2019) - 2018
- [j8]Jinghao Shi
Wireless protocol validation under uncertainty. Formal Methods Syst. Des. 53(1): 33-53 (2018) - [j7]Shaobo He
Verifying Relative Safety, Accuracy, and Termination for Program Approximations. J. Autom. Reason. 60(1): 23-42 (2018) - [j6]Marcelo Sousa, Isil Dillig, Shuvendu K. Lahiri:
Verified three-way program merge. Proc. ACM Program. Lang. 2(OOPSLA): 165:1-165:29 (2018) - [j5]Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, William R. Cook:
Verifying equivalence of database-driven applications. Proc. ACM Program. Lang. 2(POPL): 56:1-56:29 (2018) - [c58]Chungha Sung
Datalog-based scalable semantic diffing of concurrent programs. ASE 2018: 656-666 - [c57]Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit, Thomas W. Reps:
Code vectors: understanding programs through embedded abstracted symbolic traces. ESEC/SIGSOFT FSE 2018: 163-174 - [e2]Shuvendu K. Lahiri, Chao Wang:
Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science 11138, Springer 2018, ISBN 978-3-030-01089-8 [contents] - [d3]Jordan Henkel
Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces. Version v1.0.0. Zenodo, 2018 [all versions] - [d2]Jordan Henkel
Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces. Version v1.0.1. Zenodo, 2018 [all versions] - [d1]Jordan Henkel
Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces. Version v1.1.1. Zenodo, 2018 [all versions] - [i10]Marcelo Sousa, Isil Dillig, Shuvendu K. Lahiri:
Verifying Semantic Conflict-Freedom in Three-Way Program Merges. CoRR abs/1802.06551 (2018) - [i9]Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit, Thomas W. Reps:
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces. CoRR abs/1803.06686 (2018) - [i8]Chungha Sung, Shuvendu K. Lahiri, Constantin Enea, Chao Wang:
Datalog-based Scalable Semantic Diffing of Concurrent Programs. CoRR abs/1807.03777 (2018) - [i7]Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, Geoffrey Challen:
VeriFi: Model-Driven Runtime Verification Framework for Wireless Protocol Implementations. CoRR abs/1808.03406 (2018) - [i6]Shuvendu K. Lahiri, Shuo Chen, Yuepeng Wang, Isil Dillig:
Formal Specification and Verification of Smart Contracts for Azure Blockchain. CoRR abs/1812.08829 (2018) - [i5]Shuvendu K. Lahiri, Andrzej S. Murawski, Ofer Strichman, Mattias Ulbrich:
Program Equivalence (Dagstuhl Seminar 18151). Dagstuhl Reports 8(4): 1-19 (2018) - 2017
- [c56]Tim Wood, Sophia Drossopoulou, Shuvendu K. Lahiri, Susan Eisenbach:
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation. ESOP 2017: 937-963 - [c55]August Shi, Suresh Thummalapenta, Shuvendu K. Lahiri, Nikolaj S. Bjørner, Jacek Czerwonka:
Optimizing test placement for module-level regression testing. ICSE 2017: 689-699 - [c54]Alex Gyori, Shuvendu K. Lahiri, Nimrod Partush:
Refining interprocedural change-impact analysis using equivalence relations. ISSTA 2017: 318-328 - [c53]Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Abstract Semantic Diffing of Evolving Concurrent Programs. SAS 2017: 46-65 - [e1]Shuvendu K. Lahiri, Giles Reger:
Runtime Verification - 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings. Lecture Notes in Computer Science 10548, Springer 2017, ISBN 978-3-319-67530-5 [contents] - [i4]Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, William R. Cook:
Verifying Equivalence of Database-Driven Applications. CoRR abs/1710.07660 (2017) - 2016
- [c52]Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamaric:
Verifying Relative Safety, Accuracy, and Termination for Program Approximations. NFM 2016: 237-254 - [c51]Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, Geoffrey Challen:
Wireless Protocol Validation Under Uncertainty. RV 2016: 351-367 - [i3]Alex Gyori, Shuvendu K. Lahiri, Nimrod Partush:
Interprocedural Semantic Change-Impact Analysis using Equivalence Relations. CoRR abs/1609.08734 (2016) - 2015
- [c50]Ankush Das
Angelic Verification: Precise Verification Modulo Unknowns. CAV (1) 2015: 324-342 - [c49]Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel:
Automatic Rootcausing for Program Equivalence Failures in Binaries. CAV (1) 2015: 362-379 - [c48]Mike Barnett, Christian Bird, João Brunet, Shuvendu K. Lahiri:
Helping Developers Help Themselves: Automatic Decomposition of Code Review Changesets. ICSE (1) 2015: 134-144 - 2014
- [c47]Francesco Logozzo, Shuvendu K. Lahiri, Manuel Fähndrich, Sam Blackshear:
Verification modulo versions: towards usable verification. PLDI 2014: 294-304 - 2013
- [c46]Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo:
Towards Modularly Comparing Programs Using Automated Theorem Provers. CADE 2013: 282-299 - [c45]Sam Blackshear, Shuvendu K. Lahiri:
Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. PLDI 2013: 209-218 - [c44]Chris Hawblitzel, Shuvendu K. Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth:
Will you still compile me tomorrow? static cross-version compiler validation. ESEC/SIGSOFT FSE 2013: 191-201 - [c43]Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel:
Differential assertion checking. ESEC/SIGSOFT FSE 2013: 345-355 - [c42]Julien Vanegue, Shuvendu K. Lahiri:
Towards Practical Reactive Security Audit Using Extended Static Checkers. IEEE Symposium on Security and Privacy 2013: 33-47 - 2012
- [c41]Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri:
A Solver for Reachability Modulo Theories. CAV 2012: 427-443 - [c40]Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo:
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. CAV 2012: 712-717 - [c39]Saurabh Joshi, Shuvendu K. Lahiri, Akash Lal:
Underspecified harnesses and interleaved bugs. POPL 2012: 19-30 - 2011
- [c38]Shuvendu K. Lahiri:
SMT-Based Modular Analysis of Sequential Systems Code. CAV 2011: 21-27 - [c37]Patrice Godefroid, Shuvendu K. Lahiri:
From Program to Logic: An Introduction. LASER Summer School 2011: 31-44 - [c36]Shuvendu K. Lahiri, Shaz Qadeer:
Call Invariants. NASA Formal Methods 2011: 237-251 - [c35]Shuvendu K. Lahiri, Shaz Qadeer, David Walker
Linear maps. PLPV 2011: 3-14 - [c34]Patrice Godefroid, Shuvendu K. Lahiri, Cindy Rubio-González:
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation. SAS 2011: 112-128 - [c33]Shuvendu K. Lahiri, Julien Vanegue:
ExplainHoudini: Making Houdini Inference Transparent. VMCAI 2011: 309-323 - 2010
- [c32]Shuvendu K. Lahiri, Kapil Vaswani, C. A. R. Hoare:
Differential static analysis: opportunities, applications, and challenges. FoSER 2010: 201-204 - [c31]Shuvendu K. Lahiri, Alexander Malkis
Abstract Threads. VMCAI 2010: 231-246 - [c30]Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, Julien Vanegue:
Towards Scalable Modular Checking of User-Defined Properties. VSTTE 2010: 1-24
2000 – 2009
- 2009
- [j4]Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric:
A low-level memory model and an accompanying reachability predicate. Int. J. Softw. Tools Technol. Transf. 11(2): 105-116 (2009) - [c29]Shuvendu K. Lahiri, Shaz Qadeer:
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. CADE 2009: 214-229 - [c28]Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies:
Intra-module Inference. CAV 2009: 493-508 - [c27]Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric:
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. CAV 2009: 509-524 - [c26]Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer:
Unifying type checking and property checking for low-level code. POPL 2009: 302-314 - 2008
- [c25]Chao Wang, Malay K. Ganai, Shuvendu K. Lahiri, Daniel Kroening
Embedded software verification: challenges and solutions. ICCAD 2008: 5 - [c24]Carlos Pacheco, Shuvendu K. Lahiri, Thomas Ball:
Finding errors in .net with feedback-directed random testing. ISSTA 2008: 87-96 - [c23]Shuvendu K. Lahiri, Shaz Qadeer:
Back to the future: revisiting precise program verification using SMT solvers. POPL 2008: 171-182 - 2007
- [j3]Shuvendu K. Lahiri, Krishna K. Mehra:
Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic. J. Satisf. Boolean Model. Comput. 1(3-4): 187-207 (2007) - [j2]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. Log. Methods Comput. Sci. 3(2) (2007) - [j1]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1): 4 (2007) - [c22]Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, Thomas Ball:
Feedback-Directed Random Test Generation. ICSE 2007: 75-84 - [c21]Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric:
A Reachability Predicate for Analyzing Low-Level Software. TACAS 2007: 19-33 - 2006
- [c20]Shuvendu K. Lahiri, Madanlal Musuvathi:
Solving Sparse Linear Constraints. IJCAR 2006: 468-482 - [c19]Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
SMT Techniques for Fast Predicate Abstraction. CAV 2006: 424-437 - [c18]Shuvendu K. Lahiri, Shaz Qadeer:
Verifying properties of well-founded linked lists. POPL 2006: 115-126 - [i2]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. CoRR abs/cs/0612003 (2006) - 2005
- [c17]Shuvendu K. Lahiri, Thomas Ball, Byron Cook:
Predicate Abstraction via Symbolic Decision Procedures. CAV 2005: 24-38 - [c16]Shuvendu K. Lahiri, Madanlal Musuvathi:
An Efficient Decision Procedure for UTVPI Constraints. FroCoS 2005: 168-183 - [c15]Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi:
Zap: Automated Theorem Proving for Software Analysis. LPAR 2005: 2-22 - [c14]Shuvendu K. Lahiri, Madanlal Musuvathi:
An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals. PDPAR@CAV 2005: 27-41 - 2004
- [c13]Shuvendu K. Lahiri, Randal E. Bryant:
Indexed Predicate Discovery for Unbounded System Verification. CAV 2004: 135-147 - [c12]Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang:
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. CAV 2004: 457-461 - [c11]Shuvendu K. Lahiri, Sanjit A. Seshia:
The UCLID Decision Procedure. CAV 2004: 475-478 - [c10]Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur:
Revisiting Positive Equality. TACAS 2004: 1-15 - [c9]Shuvendu K. Lahiri, Randal E. Bryant:
Constructing Quantified Invariants via Predicate Abstraction. VMCAI 2004: 267-281 - [i1]Shuvendu K. Lahiri, Randal E. Bryant:
Predicate Abstraction with Indexed Predicates. CoRR cs.LO/0407006 (2004) - 2003
- [c8]Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
A Symbolic Approach to Predicate Abstraction. CAV 2003: 141-153 - [c7]Shuvendu K. Lahiri, Randal E. Bryant:
Deductive Verification of Advanced Out-of-Order Microprocessors. CAV 2003: 341-353 - [c6]Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Convergence Testing in Term-Level Bounded Model Checking. CHARME 2003: 348-362 - [c5]Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant:
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. DAC 2003: 425-430 - 2002
- [c4]Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia:
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. CAV 2002: 78-92 - [c3]Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant:
Modeling and Verification of Out-of-Order Microprocessors in UCLID. FMCAD 2002: 142-159 - 2001
- [c2]Shuvendu K. Lahiri, Carl Pixley, Ken Albin:
Experience with term level modeling and verification of the M*CORE TM microprocessor core. HLDVT 2001: 109-114
1990 – 1999
- 1999
- [c1]Partha Pratim Chakrabarti, Pallab Dasgupta, Partha Pratim Das, Arnob Roy, Shuvendu K. Lahiri, Mrinal Bose:
Controlling State Explosion in Static Simulation by Selective Composition. VLSI Design 1999: 226-231
Coauthor Index
Madan Musuvathi
aka: Madanlal Musuvathi
aka: Madanlal Musuvathi
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-13 20:03 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: