- Differential program analysis (e.g. SymDiff project)
- Scalable program verification for production software (e.g. Angelic Verifier and HAVOC projects)
Earlier projects
About
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. Earlier, I obtained my PhD from Carnegie Mellon University, and my B.Tech. from Indian Institute of Technology, Kharagpur, India.
Projects
Publications
Other
Awards
- 10-year Most Influential Paper Award for ICSE 2007 paper at International Conference on Software Engineering 2017
- Distinguished Paper Award, International Conference on Software Engineering 2017
- Best Paper Award, International Conference on Runtime Verification, 2016
- ACM 2005 Outstanding Ph.D. Dissertation Award in Electronic Design Automation.
Service
- Program Co-chair: SMT 2011, RV 2017, ATVA 2018
- Co-organizer of Dagstuhl Seminar on Program Equivalence 2018
- Program Committee member: 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
- 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.
Tutorials
- Tutorial slides at the Halmstad Summer School on Testing, 2015
- iFM 2009 Tutorial: Contract Specification and Checking: Application to .NET and C. Together with Francesco Logozzo.
- CADE 2009 Tutorial on HAVOC: Precise, Automated and Scalable Verification of Systems Software using SMT solvers. Together with Shaz Qadeer.
