Sriram K. Rajamani

Microsoft Research India

Research

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.   The Yogi project (together with  Aditya Nori, Tom Henzinger, Yamini Kannan and Bhargav Gulavani) has pioneered a new way of combining static analysis with testing.  The Netra project (together with Prasad Naldurg, Stefan Schwoon and John Lambert) uses relational analysis to analyze access control configurations of operating systems such as Windows and Linux. We are also working on several research projects in the area of software design. I will make more information available on these efforts soon.

 

I have been working on combining model checking with static program analysis techniques, decision procedures, and semi-automatic deductive methods for checking properties of both code and higher-level software models.

 

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, which is being used by product groups within Microsoft today.

 

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.