My research interests are in designing, building, and analyzing large scale computer systems in a principled manner. Over the years I have worked on various topics including Hardware and Software Verification, Type Systems, Language Design, Distributed Systems, Security and Privacy and Probabilistic Programming. Specific current research interests include:
- designing programming languages and analysis techniques to enable widespread use of machine learning by non-experts (see Probabilistic Programming).
- programming languages and tools to help with cloud security (some day I will create a page on this topic).
I list some themes from my work below:
- For the past few years, I have been working (together with Aditya Nori) on combining program analysis with statistics and machine learning (see Merlin and BayeZ projects).
- I have been interested in better abstractions to write better concurrent and distributed programs (see Clarity, Guesstimate and CScale projects)
- Verification an systematic testing form a dominant theme in my work. The SLAM project (together with Tom Ball from MSR Redmond), used model checking, theorem proving and counterexample driven refinement to check properties of system software. A tool based on SLAM called Static Driver Verifier was released as part of Windows, and is now routinely used to check if Windows Device Drivers obey their interface rules with respect to the operating system. Later, I worked with Aditya Nori on combining testing and verification (see the Yogi project ). Yogi was also used later as the verification engine inside the Static Driver Verifier. Currently, the Static Driver Verifier is being powered with the Corral verification engine (built by Akash Lal, Shaz Qadeer and Shuvendu Lahiri).
- Together with Jakob Rehof, I investigated Behavioral Type Systems to structure behaviour in asynchronous message passing programs (see Behave! project)
- Zing is an explicit state model checker (designed together with Tony Andrews, Shaz Qadeer and Jakob Rehof) for analyzing concurrent software, with modelling features that enable modelling concurrent object oriented programs with dynamic memory and threads, with support for both shared memory and message passing concurrency. Zing was used as a backend of the "P Specification language" used to design and check the USB stack that ships with Windows 8 and later.
- I have been intrigued by institutional memory present in software repositories of large projects, and investigated how to make use of this information to help programmers and testers (see DebugAdvisor)
- For my PhD thesis I worked on large-scale compositional verification of hardware chip designs. I built a model checker called Mocha (together with Shaz Qadeer and Tom Henzinger), and used it to verify a 6 million gate DSP chip.
- Before becoming a researcher, I have worked as a programmer for over five years in the USA, building and shipping various software products in telecommunication and electronic design automation. I use these first-hand experiences in realities of commercial software development to guide my choices of research problems and solutions in software productivity.