{"id":169913,"date":"2007-08-01T19:01:06","date_gmt":"2007-08-01T19:01:06","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-yogi-project\/"},"modified":"2019-11-18T15:28:14","modified_gmt":"2019-11-18T23:28:14","slug":"the-yogi-project","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-yogi-project\/","title":{"rendered":"The Yogi Project"},"content":{"rendered":"<p class=\"asset-content\"><img loading=\"lazy\" decoding=\"async\" class=\"alignleft\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/the-yogi-project-2.jpg\" alt=\"\" width=\"190\" height=\"120\" \/>Yogi is a research project within the Rigorous Software Engineering group at Microsoft Research India on software property checking. Our goal is to build a scalable software property checker by systematically combining static analysis with testing. We believe that this synergy of testing and static analysis can be harnessed to efficiently validate software.<\/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\tRelated Projects\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<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/slam\/\">SLAM<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/mtc.epfl.ch\/software-tools\/blast\/\" target=\"_self\" rel=\"noopener noreferrer\">BLAST<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/automated-test-generation-atg\/\">ATG<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/saturn.stanford.edu\/\" target=\"_self\" rel=\"noopener noreferrer\">SATURN<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/osl.cs.uiuc.edu\/~ksen\/cute\/\" target=\"_self\" rel=\"noopener noreferrer\">CUTE<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/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\tDownload Yogi for SDVRP\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><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/yogi-readme.txt\" target=\"_self\" rel=\"noopener noreferrer\">Instructions<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/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\tPeople\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<h3>Windows colleagues<\/h3>\n<ul>\n<li>Rahul Kumar<\/li>\n<li>Vladimir Levin<\/li>\n<li>Jakob Lichtenberg<\/li>\n<\/ul>\n<h3>Collaborators<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cse.iitb.ac.in\/~supratik\" target=\"_self\" rel=\"noopener noreferrer\">Supratik Chakraborty<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (IIT Bombay)<\/li>\n<li>Patrice Godefroid (MSR Redmond)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/mtc.epfl.ch\/~tah\" target=\"_self\" rel=\"noopener noreferrer\">Thomas A. Henzinger<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (EPFL)<\/li>\n<li>Akash Lal (MSR India)<\/li>\n<\/ul>\n<h3>Interns<\/h3>\n<ul>\n<li><strong>2011: <\/strong><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cs.utoronto.ca\/~aws\/\">Aws Albarghouthi<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (UToronto)<\/li>\n<li><strong>2010: <\/strong>Abhishek Katyal (IIT Delhi), Rahul Sharma (Btech thesis, IIT Delhi), Zachary Tatlock (UCSD)<\/li>\n<li><b>2009: <\/b><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/web.comlab.ox.ac.uk\/people\/Vijay.DSilva\">Vijay Victor D&#8217;Silva<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Oxford University), <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/pages.cs.wisc.edu\/~wrharris\">William Harris<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (Wisconsin), Sai Deep Tetali (UCLA)<\/li>\n<li><b>2008:<\/b> <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cse.iitb.ac.in\/~bhargav\/\">Bhargav S. Gulavani <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>(IIT Bombay), Aditya Thakur (Wisconsin)<\/li>\n<li><b>2007: <\/b><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cs.cmu.edu\/~nbeckman\/\">Nels E. Beckman <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>(CMU), <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cs.cmu.edu\/~rjsimmon\/\">Robert J. Simmons <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>(CMU)<\/li>\n<li><b>2006:<\/b> <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cse.iitb.ac.in\/~bhargav\/\">Bhargav S. Gulavani <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>(IIT Bombay), Yamini Kannan (UC Berkeley)<\/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\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n","protected":false},"excerpt":{"rendered":"<p>Yogi is a research project within the Rigorous Software Engineering group at Microsoft Research India on software property checking. Our goal is to build a scalable software property checker by systematically combining static analysis with testing.<\/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":[13561,13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-169913","msr-project","type-msr-project","status-publish","hentry","msr-research-area-algorithms","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2007-08-01","related-publications":[158295,158718,159501,159564,154429,162293,154430,154431,154432,156674,157362,158283],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[{"id":0,"name":"Tutorial","content":"<h2><a href=\"http:\/\/pldi12.cs.purdue.edu\/\">PLDI 2012<\/a> Tutorial Presentation<\/h2>\r\nSaturday, June 16, 2012, Beijing, China\r\n\r\n<strong>Tutorial slides<\/strong>\r\n<ul>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/yogi-yogi-pldi2012-tutorial-part1.pptx\" target=\"_self\">Part 1<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/yogi-yogi-pldi2012-tutorial-part2.pptx\" target=\"_self\">Part 2<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/yogi-yogi-pldi2012-tutorial-part3.pptx\" target=\"_self\">Part 3<\/a><\/li>\r\n<\/ul>\r\n<h3>Introduction<\/h3>\r\nStatic analysis and testing have always had complementary strengths and weaknesses. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable. Thus, attempting to combine the complementary strengths of static analysis and runtime testing is natural. For the past few years, we have been investigating methods for combining static analysis in the style of counter-example driven refinement ala SLAM, with runtime testing and automatic test case generation approaches in the style of concolic execution ala DART. Our first attempt in this direction was the Synergy algorithm [8], which handled single procedure programs with only integer variables. Then, we proposed the Dash algorithm [7], which had new ideas to handle pointer aliasing and procedure calls in programs. Subsequently, we proposed the Smash algorithm [4] that computes may and must information compositionally and also explains the analysis in the large and diverse amount of existing work in the area. More recently, we proposed the Bolt algorithm [1] that uses MapReduce style parallelism to scale up top-down interprocedural analyses. Throughout this evolution, Yogi has been our implementation vehicle to realize and evaluate these algorithms. We have spent over 4 person-years of engineering [5] to make the tool robust and usable. At this point, Yogi has been run over several hundreds of thousands of lines of C code\u2014in particular, it is now routinely used to verify and test several properties of Windows 7 device drivers. In this tutorial, we will present a detailed account of the evolution of Yogi and our experiences engineering this tool.\r\n<h3>Objective<\/h3>\r\nThough several verification tools are finding industrial use, the \u201c<i>secret sauce<\/i>\u201d that makes them scalable and usable is not widely known. The main objective of this tutorial is to give researchers a comprehensive picture of what it takes to design and engineer an industrial strength property checking engine. In particular, we will give:\r\n<ul>\r\n \t<li>A comprehensive treatment of Yogi\u2019s main algorithms Synergy, Dash, Smash and Bolt their evolution<\/li>\r\n \t<li>Various details of how the various algorithms in the tool have been implemented<\/li>\r\n \t<li>A description of all the optimizations built into Yogi which enables the tool to scale and work on industrial strength applications<\/li>\r\n \t<li>Extensive demos that illustrate points 1, 2 and 3. We also plan to make Yogi available for download around March 2012<\/li>\r\n<\/ul>\r\n<h3>Description of Yogi<\/h3>\r\nA detailed description of Yogi's algorithms can be found in [7, 6, 3, 2, 1]. The goal of Yogi is to solve the property checking problem. An instance of the property checking problem consists of a sequential program P and an assertion . An answer to the property checking problem is <i>pass <\/i>if every run of P satisfies the property . The answer is <i>fail<\/i> if there exists some run of P that violates .\r\n\r\nStatic analysis and testing are complementary approaches to the property checking problem. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable.\r\n\r\nOne of the unique features of Yogi is that it simultaneously searches for both a test to establish that the program violates the property, and an abstraction to establish that the program satisfies the property. If the abstraction has a path that leads to the violation of the property, Yogi attempts to focus test case generation along that path. If such a test case cannot be generated, Yogi uses information from the unsatisfiable constraint from the test case generator to refine the abstraction. Thus, the construction of test cases and abstraction proceed hand-in-hand, using error traces in the abstraction to guide test case generation, and constraints from failed test-case generation attempts to guide refinement of the abstraction.\r\n\r\nWe have engineered Yogi in such a way that it plugs into Microsoft's <a href=\"http:\/\/msdn.microsoft.com\/en-us\/windows\/hardware\/gg487498\" target=\"_blank\" rel=\"noopener\">Static Driver Verifier<\/a> (SDV) framework. We have used this framework to run Yogi on several Windows 7 device drivers and properties.\r\n<h3>Topics covered<\/h3>\r\n<ul>\r\n \t<li>\r\n<div>Overview of the current state-of-the-art in property checking \u2013 software model checking tools and testing tools<\/div><\/li>\r\n \t<li>\r\n<div>Description of the Synergy, Dash, Smash and Bolt algorithms<\/div><\/li>\r\n \t<li>\r\n<div>Architecture of Yogi and integration with Microsoft\u2019s Static Driver Verifier (SDV) toolkit<\/div><\/li>\r\n \t<li>\r\n<div>Engineering optimizations in Yogi \u2013 details on what works and what does not work<\/div><\/li>\r\n<\/ul>\r\n<h3>Target audience<\/h3>\r\nThe target audience includes faculty, graduate students and undergraduate students and anybody who is concerned about software reliability and program correctness."}],"slides":[],"related-researchers":[{"type":"user_nicename","value":"adityan","display_name":"Aditya Nori","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/adityan\/\" aria-label=\"Visit the profile page for Aditya Nori\">Aditya Nori<\/a>","is_active":false,"user_id":30829,"last_first":"Nori, Aditya","people_section":0,"alias":"adityan"},{"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],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169913"}],"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":6,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169913\/revisions"}],"predecessor-version":[{"id":621744,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169913\/revisions\/621744"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=169913"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=169913"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=169913"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=169913"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=169913"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}