I am a Principal 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.


Checked C

The Checked C research project is investigating how to extend the C programming language so that programmers can write more secure and reliable C programs. The project is developing an extension to C called Checked C that adds checking to C to detect or prevent common programming errors such as buffer overruns, out-of-bounds memory accesses, and incorrect type casts. The extension is designed to be used for existing system software written in C. Finding out…

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 assertion checking for any developer. Technically, this translates to finding precise interprocedural defect traces of assertion violations in open programs with under constrained environment (inputs and external methods). The philosophy of AV is to provide…

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 and fixed number of context switches. Corral also supports the Duality extension for constructing inductive proofs of correctness of programs. New: Microsoft Static Driver Verifier Benchmarks Corral powers Microsoft's Static Driver Verifier tool. This work has…

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 properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications…

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 Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes…


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 and arrays. The main challenge addressed by the tool are (1) tradeoff between expressiveness of the assertion logic and its computational efficiency, (2) generic inference techniques to relieve users of annotation burden for large modules.









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


Abstract Threads
Shuvendu Lahiri, Alexander Malkis, Shaz Qadeer, in Conference on Verification, Model Checking, and Abstract Interpretation, Springer Verlag, January 1, 2010, View abstract








December 2012

    Click the icon to access this download

  • Website

HAVOC: Heap-Aware Verifier for C Programs

June 2008

    Click the icon to access this download

  • Website



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.