Shaz Qadeer's Home Page

Contact information Address: One Microsoft Way, Redmond, WA 98052 Email: last_name@microsoft.com Phone: (425) 707-9146 Fax: (425) 936-7329 Research interests I am a member of the Software Reliability Research group at Microsoft Research. My work aims to improve software reliability by providing programmers with automated tools to analyze their programs.  I am interested in a variety of program analysis techniques, such as model checking, automated theorem proving, type systems, and run-time verification. Most of my work has focused on applying these techniques to analysis of concurrent software.

NEW!

• Taming concurrency: A program verification perspective
  • Distinguished Lecture, Computer Science Department, Princeton University, December 2007
  • Invited Lecture, International Conference on Concurrency Theory (CONCUR), August 2008
• HAVOC: A precise and scalable verifier for systems software
• Algorithmic verification of concurrent programs, Invited Lectures, MSR India Summer School on Programming Languages, Analysis and Verification, June 2008.

Projects

• CHESS
• HAVOC

The following list contains my recent publications.  A complete list of my publications can be found here.

• J. Condit, B. Hackett, S. K. Lahiri, and S. Qadeer. Unifying type checking and property checking for low-level code. Proceedings of the 36th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, 2009. Abstract Pdf
• T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. Proceedings of the 36th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, 2009. Abstract Pdf
• M. Musuvathi, S. Qadeeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. Proceedings of the 8th USENIX Symposium on Operating System Design and Implementation, 2008. Abstract Pdf
• M. Musuvathi and S. Qadeer. Fair stateless model checking. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2008. Abstract Pdf
• S. K. Lahiri and S. Qadeer. Back to the future: Revisiting precise program verification using SMT solvers. Proceedings of the 35th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, 2008. Abstract Pdf
• A. Bouajjani, S. Fratani, and S. Qadeer. Context-bounded analysis of multithreaded programs with dynamic linked structures. Proceedings of the 19th International Conference on Computer Aided Verification, 2007. Abstract Pdf
• M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007. Abstract Pdf
• T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: A race and transaction-aware Java runtime. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007. Abstract Pdf
• S. Chatterjee, S.K. Lahiri, S. Qadeer and Z. Rakamaric. A reachability predicate for analyzing low-level software. Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2007. Abstract Pdf

• ECI 2007: Lecture 0, Lecture 1, Lecture 2, Lecture 3, Lecture 4, Lecture 5, Lecture 6, Lecture 7.
• CSE 599f: Formal Verification of Computer Systems Course web page
• Debugging concurrent programs by context-bounded analysis.  Powerpoint
• Atomicity: A powerful concept for analyzing concurrent software. Presented at the Purdue CS Department Colloquium, April 2004. Powerpoint
• Summarizing procedures in concurrent programs. Presented at the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2004. Powerpoint
• Types for atomicity in multithreaded software.  Presented at MIT EECS Colloquium on Compilers and Architectures, March 2003. Powerpoint.
• Predicate abstraction for software verification. Presented at the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2002. Powerpoint.
• Modular verification of multithreaded software. Presented at the ESD seminar at UC Berkeley and at the CS Department, Stanford University, October 2001. Powerpoint
• Thread modular verification. University of Washington and Microsoft Research Summer Institute, August 2001. Powerpoint
• Verification of Architectural Memory Models by Model Checking. Presented at Microsoft Research and University of Washington, December 2000. Powerpoint
• Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. Tutorial presented at International Conference on Computer-Aided Design, November 2000.
  1. Part I powerpoint (courtesy T. A. Henzinger)
  2. Part II powerpoint (courtesy S. K. Rajamani)
• Algorithms and Methodology for Scalable Model Checking. Spring 1999. Powerpoint