madanm | SRR | MSR | Microsoft

 

  home | current research | people | search | news | publications | downloads | opportunities | labs | visit msr

 

 

madanm.jpg

Madan Musuvathi

Researcher
Software Reliability Research, Microsoft Research

E-mail

\com\microsoft\madanm

Office:

(425) 706-5946

FAX:

(425) 936-7329

Mail:

One Microsoft Way, Redmond, WA 98052

 

Research

I am a researcher in the Software Reliability Research group at Microsoft Research. I am broadly interested in the verification and the analysis of large scale systems. Most of my research involves building automated tools to analyze programs, both to find errors and to provide qualified correctness guarantees to the user.

New

·         CHESS is available for download

·         PC member, SPIN 2008

Projects

·         CHESS is a tool for finding errors in multi-threaded programs. CHESS uses model checking techniques to effectively search the state space of real programs.

·         FeatherLite is a light-weight data-race detection tool.

·         SoBeR is a tool for finding relaxed-memory model errors in programs.

·         Zap is an automated theorem prover for program verifications.

·         Probit is an automated test generation tool.

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).

Selected Publications

·         Effective Program Verification for Relaxed Memory Models, S. Buckhardt, M. Musuvathi. Microsoft Research Technical Report, MSR-TR-2008-12, 2008. To appear in CAV 2008.

This paper describes a novel technique for finding errors arising from relaxed memory models by only exploring sequentially consistent executions. This means that one can very easily extend existing verification techniques (such as stateless model checking, bounded model checking) to find relaxed memory model problems with no additional cost.

 

·         Fair Stateless Model Checking, M. Musuvathi, S. Qadeer. To appear in PLDI 2008.

This paper extends the stateless model checking algorithm for nonterminating programs, by incorporating a fair but sufficiently demonic scheduler. This allows us to use a tool like CHESS to find livelocks in concurrent programs. 

 

·         Iterative Context Bounding for Systematic Testing of Multithreaded Programs, M. Musuvathi, S. Qadeer. In ACM Conference on Programming Language Design and Implementation (PLDI ’07), June 2007.

This paper proposes a new prioritized algorithm for searching the large state space of multithreaded programs. The algorithm explores those executions with a fewer number of preemptions first. This paper demonstrates that this algorithm is very effective in detecting bugs without getting swamped by state space explosion. It also provides a valuable semantic notion of test-coverage for multithreaded programs.

 

·         Using Model Checking to Find Serious File System Errors. Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi. In Proceedings of the Sixth Symposium on Operating Systems Design and Implementation (OSDI '04), December 2004.This paper received the "Best Paper Award" in OSDI 2004. 

Publications

All my publications are available here.