My research interests are in improving the productivity of designing, building and deploying large scale software.

Our research group (RSE) does research with the goal of dramatically improving productivity of building software, by bringing rigor to all aspects of software development. I am currently working in 3 areas:

1. Combining program analysis with statistics and machine learning(Merlin and BayeZ projects)
2. New programming abstractions to write better concurrent and distributed programs (Clarity, Guesstimate and CScale projects)
3. Combining testing and verification (mainly, the Yogi project )

My most successful project has been the SLAM project (together with Tom Ball from MSR Redmond), which used model checking, theorem proving and counterexample driven refinement to check properties of system software. A tool based on SLAM called Static Driver Verifier is being released as part of Windows Vista, and is now routinely used to check if Windows Device Drivers obey their interface rules with respect to the operating system.

The Behave! project (together with Jakob Rehof) uses behavioral type systems to find errors in asynchronous message passing programs. Zing is a new model checking infrastructure (together with Tony Andrews, Shaz Qadeer and Jakob Rehof) for analyzing concurrent software

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.