{"id":325037,"date":"2016-11-20T23:16:16","date_gmt":"2016-11-21T07:16:16","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=325037"},"modified":"2019-11-19T11:02:20","modified_gmt":"2019-11-19T19:02:20","slug":"angelic-verification","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/angelic-verification\/","title":{"rendered":"Angelic Verification"},"content":{"rendered":"<p>Angelic verification (AV) is a project for bringing the benefits of <strong><em>static assertion checking<\/em> <\/strong>to <strong><em>production software<\/em> <\/strong>without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize\u00a0static assertion checking for <em>any developer<\/em>.<\/p>\n<p>Technically, this translates to finding <span style=\"text-decoration: underline;\"><em>precise interprocedural defect traces<\/em> <\/span>of assertion violations in <span style=\"text-decoration: underline;\"><em>open programs<\/em> <\/span>with under constrained environment (inputs and external methods). The philosophy of AV is to provide an &#8220;out-of-the-box&#8221; experience where the verifier provides high-quality warnings (aka, no &#8220;dumb warnings&#8221;) to the user, and has a &#8220;pay-as-you-go&#8221; model where more modeling can lead to more high-quality violations. AV achieves this vision by looking for angelic\/reasonable specifications on the environment that suppresses the warning, and reports a warning only when no such specification can be found. The research questions in AV include how to identify the vocabulary of specifications that can be (a) efficiently searched,\u00a0 (b) can retain a few high-quality warnings, and (c) be extensible by a user. AV has been applied on both Microsoft and open-source software (using SMACK) to find high-quality memory safety defects with almost zero domain-knowledge of the software component.<\/p>\n<p>The AV source code is part of the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/boogie-org\/corral\" target=\"_blank\" rel=\"noopener noreferrer\">Corral GitHub enlistment\u00a0<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>and parts of\u00a0it ship with the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v=vs.85).aspx\" target=\"_blank\" rel=\"noopener noreferrer\">Static Driver Verifier <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>tool in Windows (e.g. the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/mt779102(v=vs.85).aspx\" target=\"_blank\" rel=\"noopener noreferrer\">Nullcheck rule <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>powered by AV).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Angelic verification (AV) brings the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static assertion checking for any developer.<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-325037","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":"2015-01-01","related-publications":[509975,418112,168251,164254,161858,674928],"related-downloads":[489197],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Akash Lal","user_id":30905,"people_section":"Researcher team","alias":"akashl"},{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Researcher team","alias":"shuvendu"},{"type":"guest","display_name":"Shaobo He","user_id":621945,"people_section":"Interns","alias":""},{"type":"guest","display_name":"Yi Li","user_id":621948,"people_section":"Interns","alias":""},{"type":"guest","display_name":"Alexander Nutz","user_id":621951,"people_section":"Interns","alias":""}],"msr_research_lab":[199562],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/325037"}],"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\/325037\/revisions"}],"predecessor-version":[{"id":622008,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/325037\/revisions\/622008"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=325037"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=325037"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=325037"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=325037"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=325037"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}