Zing is a flexible and scalable infrastructure for exploring states of concurrent software systems. This infrastructure can be used for validating software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows and Windows Phone.

Sources

Source code is now available through Codeplex for use and modification/experimentation by research community.

Papers

• A. Udupa, A. Desai, S. K. Rajamani, Depth bounded explicit state model checking, in SPIN 2011. pdf
• M. Emmi, S. Qadeer, Z. Rakamaric, Delay-bounded scheduling, in POPL 2011. available here
• T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie, Zing: Exploiting Program Structure for Model Checking Concurrent Software, in CONCUR 2004. pdf
• T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie, Zing: A Model Checker for Concurrent Software, MSR Technical Report: MSR-TR-2004-10. pdf

• V. Levin, R. Palmer, S. Qadeer and S. K. Rajamani, Sound Transaction-based Reduction Without Cycle Detection, MSR Technical Report: MSR-TR-2005-40. available here

• S. Qadeer and S. K. Rajamani, Deciding Assertions in Programs with References, MSR Technical Report: MSR-TR-2005-08. available here
• S. Qadeer, S. K. Rajamani, and J. Rehof, Summarizing Procedures in Concurrent Programs, in POPL 2004. pdf

• M. Musuvathi and D. Dill, An Incremental Heap Canonicalization Algorithm, MSR Technical Report: MSR-TR-2005-37. available here

• C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof, Stuck-free Conformance, in CAV 2004. pdf
• C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof, Stuck-free Conformance Theory for CCS, MSR Technical Report: MSR-TR-2004-69. available here

Presentations

• Zing: Exploiting Program Structure for Model Checking Concurrent Software presented at CONCUR 2004.
• Zing: A Systematic State Explorer for Concurrent Software a slide-deck with an overview of the entire project
• Summarizing Procedures in Concurrent Programs presented at Dagstuhl Seminar on Applied Deductive Verification 2003
• Summarizing Procedures in Concurrent Programs presented at ACM Symposium on Principles of Programming Languages, 2004

People

• Ankush Desai
• Shaz Qadeer
• Sriram K. Rajamani

Alumni

• Tony Andrews
• Madan Musuvathi
• Jakob Rehof

Contact

Please send inquiries about the Zing project to zing at microsoft dot com