{"id":169916,"date":"2003-12-08T11:08:46","date_gmt":"2003-12-08T19:08:46","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/zing\/"},"modified":"2017-06-21T09:17:38","modified_gmt":"2017-06-21T16:17:38","slug":"zing","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/zing\/","title":{"rendered":"Zing"},"content":{"rendered":"<p><span id=\"dcd4de43-c047-4d74-92ae-25df1d7f8645\" class=\"ImageBlock fn\"><img decoding=\"async\" id=\"Imagedcd4de43-c047-4d74-92ae-25df1d7f8645\" class=\"alignleft\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-image002.jpg\" alt=\"\" \/><span id=\"ImageCaptiondcd4de43-c047-4d74-92ae-25df1d7f8645\" class=\"ImageCaptionCoreCss ImageCaption\"><\/span><\/span><\/p>\n<p>Zing is a\u00a0flexible and scalable\u00a0infrastructure for exploring\u00a0states of concurrent software systems.\u00a0This infrastructure can be used for\u00a0validating software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system.\u00a0Zing\u00a0is\u00a0currently\u00a0being used for developing drivers for Windows and Windows Phone.<\/p>\n<h1>Sources<\/h1>\n<p><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/zing.codeplex.com\/\" target=\"_self\"><b>Source code<\/b><\/a> is now available through <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/zing.codeplex.com\/\" target=\"_self\"><strong>Codeplex<\/strong><\/a>\u00a0for use and modification\/experimentation by research community.<\/p>\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-1\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-1\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-2\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-2\">\n\t\tDocumentation\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-2\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<h1>Papers<\/h1>\n<ul>\n<li>A. Udupa, A. Desai, S. K. Rajamani, <strong>Depth bounded explicit state model checking<\/strong>, in SPIN 2011. <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/tr-11.pdf\" target=\"_self\">pdf<\/a><\/li>\n<li>M. Emmi, S. Qadeer, Z. Rakamaric, <strong>Delay-bounded scheduling<\/strong>, in POPL 2011.<\/li>\n<li>T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie, <b>Zing: Exploiting Program Structure for Model Checking Concurrent Software<\/b>, <em>in CONCUR 2004.<\/em>\u00a0<a title=\"\" href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-zingconcur.pdf\" target=\"_self\">pdf<\/a><\/li>\n<li>T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie, <b>Zing: A Model Checker for Concurrent Software<\/b>, <i>MSR Technical Report: MSR-TR-2004-10. <\/i><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-tool.pdf\" target=\"_self\">pdf<\/a><\/li>\n<li>V. Levin, R. Palmer, S. Qadeer and S. K. Rajamani, <b>Sound Transaction-based Reduction Without Cycle Detection<\/b>, <i>MSR Technical Report: MSR-TR-2005-40. <\/i><\/li>\n<li>S. Qadeer and S. K. Rajamani, <b>Deciding Assertions in Programs with References<\/b>, <i>MSR Technical Report: MSR-TR-2005-08. <\/i><\/li>\n<li>S. Qadeer, S. K. Rajamani, and J. Rehof, <b>Summarizing Procedures in Concurrent Programs<\/b>, <em>in POPL 2004. <\/em>pdf<\/li>\n<li>M. Musuvathi and D. Dill, <b>An Incremental Heap Canonicalization Algorithm<\/b>, <i>MSR Technical Report: MSR-TR-2005-37. <\/i><\/li>\n<li>C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof, <b>Stuck-free Conformance<\/b>,<em> in CAV 2004.<\/em> <a title=\"\" href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-stuckfreeconformance.pdf\" target=\"_self\">pdf<\/a><\/li>\n<li>C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof, <b>Stuck-free Conformance Theory for CCS<\/b>,<i> MSR Technical Report: MSR-TR-2004-69. <\/i><\/li>\n<\/ul>\n<h1>Presentations<\/h1>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-zingconcur2004.ppt\"><b><i>Zing: Exploiting Program Structure for Model Checking Concurrent Software <\/i><\/b><\/a>presented at CONCUR 2004.<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-zing-overview.ppt\"><b><i>Zing: A Systematic State Explorer for Concurrent Software <\/i><\/b><\/a>a slide-deck with an overview of the entire project<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-summarization.ppt\"><b><i>Summarizing Procedures in Concurrent Programs<\/i><\/b><\/a>\u00a0presented at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.dagstuhl.de\/03451\/\">Dagstuhl Seminar on Applied Deductive Verification 2003<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/zing-popl04.ppt\"><b><i>Summarizing Procedures in Concurrent Programs<\/i><\/b><\/a> presented at ACM Symposium on Principles of Programming Languages, 2004<\/li>\n<\/ul>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-3\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-3\">\n\t\tAlumni\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-3\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<ul>\n<li>Tony Andrews<\/li>\n<li>Madan Musuvathi<\/li>\n<li>Jakob Rehof<\/li>\n<\/ul>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-4\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-4\">\n\t\tContact\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-4\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<p>Please send inquiries about the Zing project to zing <i>at<\/i> microsoft <i>dot<\/i> com<\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n","protected":false},"excerpt":{"rendered":"<p>Zing is a\u00a0flexible and scalable\u00a0infrastructure for exploring\u00a0states of concurrent software systems.\u00a0This infrastructure can be used for\u00a0validating software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system.\u00a0Zing\u00a0is\u00a0currently\u00a0being used for developing drivers for Windows and Windows Phone. Sources Source code is now available through Codeplex\u00a0for [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-169916","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2003-12-08","related-publications":[160695],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","value":"sriram","display_name":"Sriram Rajamani","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\" aria-label=\"Visit the profile page for Sriram Rajamani\">Sriram Rajamani<\/a>","is_active":false,"user_id":33711,"last_first":"Rajamani, Sriram","people_section":0,"alias":"sriram"}],"msr_research_lab":[199562,199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169916"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":5,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169916\/revisions"}],"predecessor-version":[{"id":392459,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169916\/revisions\/392459"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=169916"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=169916"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=169916"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=169916"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=169916"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}