madanm | SRR | MSR | Microsoft
home | current research | people | search | news | publications | downloads | opportunities | labs | visit msr

	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 interested in the analysis of complex and large-scale systems. My research is inter-disciplinary and includes systems, networking, 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.

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

New

· OSDI ’08 paper that describes the CHESS architecture is available.

· See CHESS at Microsoft PDC

· CHESS is available for download

Projects

· CHESS is a tool for finding and reproducing Heisenbugs in concurrent 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.

Selected Publications

· Finding and Reproducing Heisenbugs in Concurrent Programs, Madanlal Musuvathi, Shaz Qadeer, Tom Ball, Gerard Basler, P. Arumuga Nainar, Iulian Neamtiu. To appear in OSDI ’08.

This paper describes the architecture of CHESS, a tool for finding and reproducing concurrency bugs that are otherwise hard to find, debug, and eliminate. The architecture allows CHESS to scale to multiple platforms: Win32, .NET, and Singularity. The paper describes some of the cool bugs we found with CHESS.

· Effective Program Verification for Relaxed Memory Models, Sebastian Buckhardt, Madanlal Musuvathi. 20^th International Conference on Computer Aided Verification (CAV ‘08), July 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, Madanlal Musuvathi, Shaz Qadeer. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08), June 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, Madanlal Musuvathi, Shaz Qadeer. In ACM SIGPLAN 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.