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.


Angelic Verification

Established: January 1, 2015

Angelic verification (AV) is a project for bringing the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static…

Corral Program Verifier

Established: May 9, 2013

Corral is a whole-program analysis tool for Boogie programs. Corral uses goal-directed symbolic search techniques to find assertion violations. It leverages the powerful theorem prover Z3. It is available open source on GitHub. Corral, by default, does a bounded search up to a recursion depth…

SymDiff: Differential program verifier

Established: October 14, 2010

SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential/relational…

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…


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…








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








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.