Publications

Stateless Model Checking

• Effective Program Verification for Relaxed Memory Models, S. Buckhardt, M. Musuvathi. Microsoft Research Technical Report, MSR-TR-2008-12, 2008
• Fair Stateless Model Checking, M. Musuvathi, S. Qadeer. To appear in PLDI ‘08.
• 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.

Satisfiability Modulo Theories

• Solving Sparse Linear Constraints, S. K. Lahiri, M. Musuvathi. In 3rd International Joint Conference on Automated Reasoning (IJCAR), August, 2006, Seattle.
• Zap: Automated Theorem Proving for Software Analysis. T. Ball, S. K. Lahiri, M. Musuvathi, Microsoft Research Technical Report MSR-TR-2005-137, October 2005. In 12th International Conference on Logic for Programming, Aritificial Intelligence and Reasoning (LPAR '05).
• A Combination Method for Generating Interpolants. G. Yorsh and M. Musuvathi, In the Twentieth International Conference on Automated Deduction (CADE '05) , July 2005.
• An Efficient Decision Procedure for UTVPI Constraints. S. Lahiri, M. Musuvathi, In Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (ForCos ’05), Vienna, Austria, Sept 2005.
• An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals. S. Lahiri, M. Musuvathi, In Proceedings of Third Workshop on Pragmatics of Decision Procedures in Automated Reasonsing (PDPAR ’05), Scotland, July 2005.
• A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. K. R. M. Leino, M. Musuvathi, X. Ou. In the Eleventh Conference on Tools and Algorithms for the Construction and Analysis of Software (TACAS '05), April 2005.

Model Checking C Programs

• An Incremental Heap Canonicalization Algorithm. M. Musuvathi, D. L. Dill, In the Twelfth International SPIN workshop on Model Checking of Software (SPIN '05), August 2005.
• Using Model Checking to Find Serious File System Errors. J. Yang, P. Twohey, D. Engler, and M. Musuvathi. In Proceedings of the Sixth Symposium on Operating Systems Design and Implementation (OSDI), December 2004.
• Model-checking large network protocol implementations. M. Musuvathi, D. Engler. Proceedings of the First Conference on Network System Design and Implementation (NSDI), 2004.
• Static analysis versus software model checking for bug finding. D. Engler, M. Musuvathi. Invited paper for VMCAI '04.
• Some lessons from using static analysis and software model checking for bug finding. M. Musuvathi, D. Engler. In the Software Model Checking (SoftMC) Workship 2003.
• CMC: A pragmatic approach to model checking real code. M. Musuvathi, D. Y.W. Park, A. Chou, D. Engler, D. L. Dill.  In Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (OSDI), December 2002.