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
• Concurrency Fuzzing
• Memory Models
• CHESS

Professional Activities

• Chair: WODA 2012, MSPC 2011, SPIN 2011, SAVCBS 2010
• Steering Committee: WODA, MSPC
• Program Committee: PPoPP 2014, SPIN 2013, (EC)2, PLDI 2013 (ERC), PPoPP 2013 (ERC),  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, Ohad Shacham, Samira Tashoraffi

Theses

• Simplified Semantics and Debugging of Concurrent Programs via Targeted Race Detection, Daniel Marino, co-advised by Todd Millstein (2012 ACM SIGPLAN Outstanding Doctoral Dissertation Award)
• Fast Error Detection with Coverage Guarantees for Concurrent Software, Katie Coons, co-advised by Kathryn McKinley

Selected/Recent Publications

(All my publications are available here.)

• [ISCA '12] (IEEE Top-Picks) 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?
• [ESOP '12] Concurrent Library Correctness on the TSO Memory Model
• [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 

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

Lectures

• Invited Tutorial on Dynamic Data Race Detection at RV 2012
• 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).