{"id":170904,"date":"2012-02-07T15:13:49","date_gmt":"2012-02-07T15:13:49","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/duality\/"},"modified":"2016-06-01T15:40:15","modified_gmt":"2016-06-01T22:40:15","slug":"duality","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/duality\/","title":{"rendered":"Duality"},"content":{"rendered":"<p>Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of manual proofs.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of [&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-170904","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":"2012-02-07","related-publications":[164169,166673],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","value":"akashl","display_name":"Akash Lal","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/akashl\/\" aria-label=\"Visit the profile page for Akash Lal\">Akash Lal<\/a>","is_active":false,"user_id":30905,"last_first":"Lal, Akash","people_section":0,"alias":"akashl"}],"msr_research_lab":[199562,199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170904"}],"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":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170904\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170904"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170904"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170904"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170904"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170904"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}