Portrait of Sriram Rajamani

Sriram Rajamani

Managing Director, Microsoft Research India Lab


Sriram Rajamani is Managing Director of Microsoft Research India. His research interests are in designing, building and analyzing computer systems in a principled manner. Over the years he has worked on various topics including Hardware and Software Verification, Type Systems, Language Design, Distributed Systems, Security and Privacy, Cloud Security and Probabilistic Programming.

Together with Tom Ball, he was awarded the CAV 2011 Award for “contributions to software model checking, specifically the development of the SLAM/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs.” Sriram was recently elected ACM Fellow  for contributions to software analysis and defect detection

Sriram has a PhD from UC Berkeley, MS from University of Virginia and BEng from  College of Engineering, Guindy, all with specialization in Computer Science. Sriram was general chair for POPL 2015 in India, and was program Co-Chair for  CAV 2005.  He co-founded the Mysore Park Series, and the ISEC conference series in India. He served on the CACM editorial board till recently.


Trusted Cloud

Established: August 31, 2015

The Trusted Cloud project at Microsoft Research aims to provide customers of cloud computing complete control over their data: no one should be able to access the data without the customer’s permission. Even if there are malicious employees in the cloud service provider, or hackers break into the data center, they still should not be able to get access to customer data. Trust model: We use a non-hierarchical trust model. That is, we don’t want…

R2: A Probabilistic Programming System

Established: July 16, 2013

What is R2? R2 is a probabilistic programming system that uses powerful techniques from program analysis and verification for efficient Markov Chain Monte Carlo (MCMC) inference. The language that is used to describe probabilistic models in R2 is based on C#.R2 compiles the given model into executable code to generate samples from the posterior distribution. The inference algorithm currently implemented in R2 is a variation of the Metropolis-Hastings sampling algorithm. Getting R2 Click on this…

Infer.NET Fun

Established: April 2, 2012

"I think it's extraordinarily important that we in computer science keep fun in computing." Alan J. Perlis - ACM Turing Award Winner 1966. Infer.NET Fun turns the simple succinct syntax of F# into an executable modeling language for Bayesian machine learning. We propose a marriage of probabilistic functional programming with Bayesian reasoning. Infer.NET Fun turns F# into a probabilistic modeling language – you can code up the conditional probability distributions of Bayes’ rule using F# array…

The Yogi Project

Established: August 1, 2007

Yogi is a research project within the Rigorous Software Engineering group at Microsoft Research India on software property checking. Our goal is to build a scalable software property checker by systematically combining static analysis with testing. We believe that this synergy of testing and static analysis can be harnessed to efficiently validate software.


Established: December 8, 2003

Zing is a flexible and scalable infrastructure for exploring states of concurrent software systems. This infrastructure can be used for validating software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows and Windows Phone. Sources Source code is now available through Codeplex for use and modification/experimentation by research community.


Established: November 5, 2001

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine. "Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas,…










Proofs from Tests
Nels E. Beckman, Aditya Nori, Sriram Rajamani, Robert J. Simmons, Sai Deep Tetali, Aditya V. Thakur, in IEEE Transactions on Software Engineering (special issue on the ISSTA 2008 best papers), IEEE, March 1, 2010, View abstract, Download PDF




Programming Asynchronous Layers with CLARITY
Prakash Chandrasekaran, Christopher L. Conway, Joseph Joy, Sriram Rajamani, in Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Association for Computing Machinery, Inc., September 1, 2007, View abstract, Download PDF








Link description

Q and A – Session 1


February 13, 2015


Jennifer Chayes, P. Anandan, Rico Malvar, Sriram Rajamani, Christopher Bishop, Victor Bahl, Raj Reddy, Ed Lazowska, and Chandu Thekkath


Microsoft, Carnegie Mellon University, University of Washington

Link description

TechVista 2012 Special Session


January 20, 2012


P. Anandan, Sriram Rajamani, Rick Rashid, Rabiranjan Chattopadhyay, and Partha Chatterjee



Prior to moving to Microsoft Research’s India lab, I was manager of the Software Productivity Tools group in Microsoft Research Redmond. I have a PhD in Computer Science from the University of California at Berkeley, MS in Computer Science from the University of Virginia, and a BE in Computer Science from Anna University College of Engineering, Guindy, in Chennai. Previously, I worked as a programmer for over 5 years writing telecommunication software and electronic design automation software. My first-hand experience in the realities of commercial software development guide my choice of problems and approaches to research in software productivity.

I’m an Adjunct Professor at the Indian Institute of Technology in Hyderabad and serve on the editorial board of CACM. I co-founded the ISEC conference in India, and serve on the executive committee of the Special Interest Group on Software Engineering (SIGSE) in India. I have also co-founded the Mysore-Park workshop series in India.

Other Interests

Together with colleagues at MSR India, I am working on a blended learning model (combining online learning with in-classroom pedagogy) for education in India. For more detais see: Massively Empowered Classrooms.

I am very interested in CS research community activities in India. See Mysore-Park workshop series.

Editorial Boards

Keynote Talks

Conference Organization

I have chaired or co-chaired the following conferences in the past. Due to my research and management workload at MSR India, I am currently not undertaking any conference chairing roles.

Program Committees

I have served on the following conference program committees:

SNAPL 2015, POPL 2013, PLDI 2013 (ERC), ISEC 2013, VMCAI 2011PLDI 2010, ICSE 2010ISEC 2010, ISSRE 2009, FSE 2009, POPL 2009FSTTCS 2008, CCS 2008, ISSTA 2008, TACAS 2008, ICSE 2008, FSE 2007, FSTTCS 2006, APLAS 2006, APSEC 2006, PLAS 2006 , POPL 2005, TACAS 2005FMCAD 2004, ISSTA 2004, FSTTCS 2003 , PPoPP 2003, CAV 2003 , TACAS 2003, SPIN 2002, FSE 2002, SAVE 2001