Travelled to:1 × Canada
1 × Denmark
1 × France
1 × Portugal
1 × Russia
17 × USA
2 × Italy
2 × Spain
2 × United Kingdom
Collaborated with:S.Qadeer R.E.Bryant C.Hawblitzel T.Ball S.A.Seshia A.Lal B.Cook S.Blackshear Z.Rakamaric C.Pacheco I.Dillig M.Kawaguchi H.Rebêlo ∅ J.Vanegue M.Musuvathi R.Sinha S.Joshi P.Godefroid C.Rubio-González A.Malkis R.Nieuwenhuis A.Oliveras M.Sousa A.Das Y.Li M.Barnett C.Bird J.Brunet F.Logozzo M.Fähndrich K.L.McMillan R.Sharma J.Condit B.Hackett M.D.Ernst S.Chatterjee L.Zhang A.Goel M.Talupur C.Sung C.Enea C.W.0001 J.Henkel B.Liblit T.W.Reps T.W.0004 S.Drossopoulou S.Eisenbach Yuepeng Wang 0001 W.R.Cook J.P.Galeotti J.W.Voung T.Wies K.Pawar H.Hashmi S.Gokbulut L.Fernando D.Detlefs S.Wadsworth
Talks about:abstract (8) predic (8) verif (8) program (7) code (5) procedur (4) modular (4) verifi (4) system (4) use (4)
Person: Shuvendu K. Lahiri
DBLP: Lahiri:Shuvendu_K=
Contributed to:
2015
2015
2014
2013
201320132012
20122011
2011
20112010200920092009
200820082007
20072006
2006200620052004200420042003
20032002
20182018
2017
20182018Wrote 41 papers:
- CAV-2015-DasLLL #precise #verification
- Angelic Verification: Precise Verification Modulo Unknowns (AD, SKL, AL, YL), pp. 324–342.
- CAV-2015-LahiriSH #automation #equivalence
- Automatic Rootcausing for Program Equivalence Failures in Binaries (SKL, RS, CH), pp. 362–379.
- ICSE-v1-2015-BarnettBBL #automation #code review #composition #developer #overview
- Helping Developers Help Themselves: Automatic Decomposition of Code Review Changesets (MB, CB, JB, SKL), pp. 134–144.
- PLDI-2014-LogozzoLFB #towards #verification
- Verification modulo versions: towards usable verification (FL, SKL, MF, SB), p. 32.
- CADE-2013-HawblitzelKLR #automation #proving #source code #theorem proving #towards #using
- Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
- ESEC-FSE-2013-HawblitzelLPHGFDW #compilation #validation
- Will you still compile me tomorrow? static cross-version compiler validation (CH, SKL, KP, HH, SG, LF, DD, SW), pp. 191–201.
- ESEC-FSE-2013-LahiriMSH #difference
- Differential assertion checking (SKL, KLM, RS, CH), pp. 345–355.
- PLDI-2013-BlackshearL #composition #framework #semantics #specification
- Almost-correct specifications: a modular semantic framework for assigning confidence to warnings (SB, SKL), pp. 209–218.
- CAV-2012-LahiriHKR #imperative #named #semantics #source code
- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs (SKL, CH, MK, HR), pp. 712–717.
- CAV-2012-LalQL #modulo theories #reachability
- A Solver for Reachability Modulo Theories (AL, SQ, SKL), pp. 427–443.
- POPL-2012-JoshiLL #debugging
- Underspecified harnesses and interleaved bugs (SJ, SKL, AL), pp. 19–30.
- CAV-2011-Lahiri #analysis #composition #smt
- SMT-Based Modular Analysis of Sequential Systems Code (SKL), pp. 21–27.
- SAS-2011-GodefroidLR #composition #generative #incremental #summary #testing #validation
- Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation (PG, SKL, CRG), pp. 112–128.
- VMCAI-2011-LahiriV #named
- ExplainHoudini: Making Houdini Inference Transparent (SKL, JV), pp. 309–323.
- VMCAI-2010-LahiriMQ #thread
- Abstract Threads (SKL, AM, SQ), pp. 231–246.
- CADE-2009-LahiriQ #abstraction #algorithm #complexity
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction (SKL, SQ), pp. 214–229.
- CAV-2009-LahiriQGVW
- Intra-module Inference (SKL, SQ, JPG, JWV, TW), pp. 493–508.
- CAV-2009-LahiriQR #concurrent #detection #fault #precise #smt #using
- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers (SKL, SQ, ZR), pp. 509–524.
- POPL-2009-ConditHLQ #low level #type checking
- Unifying type checking and property checking for low-level code (JC, BH, SKL, SQ), pp. 302–314.
- ISSTA-2008-PachecoLB #dot-net #fault #random testing #testing
- Finding errors in .net with feedback-directed random testing (CP, SKL, TB), pp. 87–96.
- POPL-2008-LahiriQ #precise #smt #using #verification
- Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.
- ICSE-2007-PachecoLEB #generative #random testing #testing
- Feedback-Directed Random Test Generation (CP, SKL, MDE, TB), pp. 75–84.
- TACAS-2007-ChatterjeeLQR #bytecode #low level #reachability
- A Reachability Predicate for Analyzing Low-Level Software (SC, SKL, SQ, ZR), pp. 19–33.
- CAV-2006-LahiriNO #abstraction #performance #smt
- SMT Techniques for Fast Predicate Abstraction (SKL, RN, AO), pp. 424–437.
- IJCAR-2006-LahiriM #constraints #linear
- Solving Sparse Linear Constraints (SKL, MM), pp. 468–482.
- POPL-2006-LahiriQ #verification
- Verifying properties of well-founded linked lists (SKL, SQ), pp. 115–126.
- CAV-2005-LahiriBC #abstraction
- Predicate Abstraction via Symbolic Decision Procedures (SKL, TB, BC), pp. 24–38.
- CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
- CAV-2004-LahiriB #bound #verification
- Indexed Predicate Discovery for Unbounded System Verification (SKL, REB), pp. 135–147.
- CAV-2004-LahiriS
- The UCLID Decision Procedure (SKL, SAS), pp. 475–478.
- TACAS-2004-LahiriBGT #similarity
- Revisiting Positive Equality (SKL, REB, AG, MT), pp. 1–15.
- VMCAI-2004-LahiriB #abstraction #invariant #quantifier
- Constructing Quantified Invariants via Predicate Abstraction (SKL, REB), pp. 267–281.
- CAV-2003-LahiriB #deduction #verification
- Deductive Verification of Advanced Out-of-Order Microprocessors (SKL, REB), pp. 341–353.
- CAV-2003-LahiriBC #abstraction #approach
- A Symbolic Approach to Predicate Abstraction (SKL, REB, BC), pp. 141–153.
- DAC-2003-SeshiaLB #hybrid #logic #satisfiability
- A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (SAS, SKL, REB), pp. 425–430.
- CAV-2002-BryantLS #logic #modelling #using #verification
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with λ Expressions and Uninterpreted Functions (REB, SKL, SAS), pp. 78–92.
- ASE-2018-SungLEW #concurrent #difference #scalability #semantics #source code
- Datalog-based scalable semantic diffing of concurrent programs (CS, SKL, CE, CW0), pp. 656–666.
- ESEC-FSE-2018-HenkelLLR #comprehension #embedded #source code
- Code vectors: understanding programs through embedded abstracted symbolic traces (JH, SKL, BL, TWR), pp. 163–174.
- ESOP-2017-WoodDLE #composition #equivalence #memory management #verification
- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (TW0, SD, SKL, SE), pp. 937–963.
- OOPSLA-2018-SousaDL
- Verified three-way program merge (MS, ID, SKL), p. 29.
- POPL-2018-0001DLC #equivalence #verification
- Verifying equivalence of database-driven applications (YW0, ID, SKL, WRC), p. 29.