Portrait of Shuvendu Lahiri

Shuvendu Lahiri

Senior Researcher

I am a Senior Researcher in the Research in Software Engineering (RiSE) Group. I am interested in the development and the application of formal methods for making program testing, verification and review (especially of production code) more scalable and automated.

Q Program Verifier

Established: May 9, 2013

The Q program verifier is a collection of front-ends that compile different source languages to an intermediate representation (IR), and back-ends that perform verification on the IR. Together, Q is a verification platform that hosts multiple tools and technologies for…

SymDiff: Differential program verifier

Established: October 14, 2010

SymDiff is an infrastructure for leveraging and extending program verification to reason about relationship between two programs (differential program analysis). There are several opportunities for differential analysis, including (a) performing incremental analysis, (b) use one program as a spec to…

Boogie: An Intermediate Verification Language

Established: December 10, 2008

Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for…

HAVOC

Established: November 25, 2008

HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists…

2016

2015

2013

2012

2011

Linear Maps
Shuvendu Lahiri, Shaz Qadeer, David Walker, in ACM SIGPLAN Workshop on Programming Languages meets Program Verification, ACM SIGPLAN, January 1, 2011, View abstract, Download PDF

2010

2009

2008

2007

2006

2005

Current projects

  • Differential program analysis [fse-sdp10][sas11][popl12][cav12-t][cade13][fse13][fse13][pldi14][icse15][cav15-a]
  • Scalable and usable program verification [cav09][cav09][vstte10][vmcai11][cav12][oakland13][pldi13][cav15-b]

Earlier projects

  • Modular reasoning about program heap [popl06][tacas07][popl08][popl09][nfm11][plpv11]
  • Automated test generation [icse07][issta08][sas11]
  • Predicate abstraction techniques  [cav03][cav04][cav05][cav06][tocl07][cade09]
  • Cache coherence protocols and microprocessor verification [hldvt01][cav02][fmcad02][cav03][vmcai04][cav04]
  • Decision procedures and SMT solvers [cav02][cfv02][dac03][cav04-t][cav04-t][tacas04][frocos05][pdpar05][lpar05][cade06][jsat06]

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.

Tutorials

​