I am a Senior Researcher in the Research in Software Engineering group at Microsoft Research.  My research focus is on scalable analysis of concurrent systems. More broadly, my interests include systems, program analysis, model checking, verification, and theorem proving. I spend a lot of time at Microsoft building analysis tools to improve the productivity of software developers and testers.

Current Research Projects

• End to End Sequential Consistency
• Probabilistic Concurrency Testing
• Memory Models
• CHESS

Professional Activities

• Chair: WODA 2012, MSPC 2011, SPIN 2011, SAVCBS 2010
• Program Committee: OOPSLA 2012 (ERC), WoDet 2012, SPIN 2012, HotPar 2012, PPoPP 2012 (ERC), WODA 2011, PADTAD 2011, CAV 2011, NFM 2010, PADTAD 2010, CC 2010, SPIN 2009, PADTAD 2009, SPIN 2008
• Organizing Committee: FLoC 2006
• Ph.D. Thesis Committee: Dan Marino, Katie Coons

Teaching

• CSE P 506: Concurrency and Parallel Programming (Spring 2011) at University of Washington, Seattle

Books

• Model Checking Software, 18th International SPIN Workshop, July 14-15, 2011

Selected/Recent Publications

(All my publications are available here.)

• [ISCA '12] End-to-end Sequential Consistency
• [PLDI '12] Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection
• [ESOP '12] What's Decidable About Weak Memory Models? (to appear)
• [ESOP '12] Concurrent Library Correctness on the TSO Memory Model (to appear)
• [SIGCOMM '11] Finding Protocol Manipulation Attacks
• [PLDI '11] A Case for an SC-Preserving Compiler
• [ASPLOS '11] Efficient Processor Support for DRFx, a Memory Model With Exceptions
• [OSDI '10] Effective Data-Race Detection for the Kernel
• [PLDI '10] Line-Up: A Complete and Automatic Linearizability Checker
• [PLDI '10] DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages
[ASPLOS '10] A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs
[POPL '10] On the Verification Problem for Weak Memory Models
[PLDI '09] LiteRace: Effective Sampling for Lightweight Data-Race Detection
[OSDI '08] Finding and Reproducing Heisenbugs in Concurrent Programs
[CAV '08] Effective Program Verification for Relaxed Memory Models
[PLDI '08] Fair stateless model checking
[PLDI '07] Iterative context bounding for systematic testing of multithreaded programs
[OSDI '04] (Best Paper) Using model checking to find serious file system errors
[OSDI '02] CMC: A pragmatic approach to model checking real code 

Lectures

• Dagstuhl Seminar: Multi-Core Memory Models and Concurrency Theory
• Lectures (1,2) at Third International School on Trends in Concurrency (May 2009)

Interns

I am always looking for interns with good systems and/or theoretical skills. Send me an email if you are interested. Here is a list of my past interns and their projects.

Biography

I obtained my M.S. and Ph.D. at Stanford University, where I worked under the guidance of Prof. David L. Dill and Prof. Dawson Engler. Before that, I got my B.Tech. in Computer Science from the Indian Institute of Technology (IIT), Chennai (which was then called Madras).