Portrait of Shuvendu Lahiri

Shuvendu Lahiri

Senior Researcher

About

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.

Projects

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. Corral powers Microsoft's Static Driver Verifier tool. This work has received several…

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…

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 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.

Publications

2017

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

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

2009

2008

2007

2006

2005

Projects

Other

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