Portrait of Shuvendu Lahiri

Shuvendu Lahiri

Principal Researcher





  • Program Co-chair: CAV2020, ATVA 2018, RV 2017SMT 2011
  • Co-organizer of Dagstuhl Seminar on Program Equivalence 2018
  • Program Committee member: POPL’20, ICSE’20, SAS’19, CAV’19, RV’18, SAS’18, CAV’18, VSTTE’17, ICSE-NIER’17, VMCAI’17, FSTTCS’16, ISEC’16, FMCAD’16, CAV’16, ICSE-NIER’16, ISEC’15, PLDI-SRC’15, SPIN’15, POPL’15 (ERC),  PLDI-SRC’14, SPIN’14, FMCAD’13, VSSE’13, SMT’12, CAV’12 (and Workshop Chair), Infinity’11, FMCAD’08, CAV’08, SMT’07, HAV’07, PDPAR’06, MEMOCODE’06.
  • Thesis Committee member: Alex Gyori (UIUC), Oswaldo Olivo (UT Austin)

Current projects

  • Specification and Verification of Blockchain Smart Contracts (e.g. VeriSol)
  • Scalable program verification for production software (e.g. Angelic Verifier)
  • Differential program analysis (e.g. SymDiff project)

Earlier projects

  • Large scale modular verification of systems programs (Havoc)
  • Modular reasoning about program heap (Havoc)
  • Automated test generation (Randoop)
  • Predicate abstraction techniques (Uclid)
  • Cache coherence protocols and microprocessor verification (Uclid)
  • Decision procedures and SMT solvers (Uclid)

In my earlier life, I was a graduate student at Carnegie Mellon University. Before that, I spent four wonderful years at the Computer Science and Engineering Dept. at the Indian Institute of Technology, Kharagpur.

PhD Thesis

Unbounded System Verification using Decision Procedure and Predicate Abstraction. Carnegine Mellon University, 2004. Winner to the ACM Outstanding Ph.D. Dissertation Award in Electronic Design Automation.