Zing is a software model checking project at Microsoft Research. Our goal is to build a flexible and scalable systematic state space exploration infrastructure for software. This infrastructure includes novel algorithms, and a modular software architecture, to push the frontier on exploring large state spaces of software. We believe that such an infrastructure can be used for verifying and finding bugs in software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system.

Downloads

Zing model checker for VS.NET 2005 (for non-commercial research use only, see EULA for details). This version of Zing has a dependency on Visual Studio .NET 2005, which is available to students and faculty in universities via the academic licensing program . Zing model checker for VS.NET 2003 (for non-commercial research use only, see EULA for details).Zing has a dependency on Visual Studio .NET 2003, which is available to students and faculty in universities via the academic licensing program . Zing language specification Overview, Examples, and reference manual for the Zing language (Word, PDF)

Zing user manual User guide for getting started with the Zing model checker (Word, PDF)

Papers

The following two papers give a broad overview of Zing.

• T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie, Zing: Exploiting Program Structure for Model Checking Concurrent Software, in CONCUR 2004. postscriptpdf
• 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. postscriptpdf

Zing uses transaction-based reduction. In transaction based reduction (as in other forms of partial order reduction), we need to avoid delaying scheduling a thread indefinitely, if we want the reduction to be sound. The following paper presents a new technique called Commit Point Completion to solve this problem.

• 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

Zing uses procedure summaries to do modular analysis. One of the novel aspects of Zing is its ability to use procedure summaries both in the presence of pointers and concurrency. The following two papers describe these techniques.

• 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.postscriptpdf

Zing uses heap canonicalization to do symmetry-reduction on the heap. We have invented a new method to canonicalize the heap incrementally, as the model checker makes transitions from states. The following paper gives details of this technique.

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

Zing uses a new theory of stuck-free conformance to do compositional checking of message passing programs. The following papers describe this theory.

• C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof, Stuck-free Conformance, in CAV 2004.postscriptpdf
• 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 Programspresented at Dagstuhl Seminar on Applied Deductive Verification 2003
• Summarizing Procedures in Concurrent Programs presented at ACM Symposium on Principles of Programming Languages, 2004

People

• Full-time Staff:
• Tony Andrews
• Madan Musuvathi
• Shaz Qadeer
• Sriram K. Rajamani
• Jakob Rehof
• Friends:
• Vlad Levin
• Summer Interns 2003:
• Abhay Gupta
• Georg Weissenbacher
• Yichen Xie
• Summer Interns 2004:
• Mayur Naik
• Robert Palmer
• Dinghao Wu

Contact Zing

Please send inquiries about the Zing project tozing at microsoft dot com