{"id":190707,"date":"2014-04-01T00:00:00","date_gmt":"2014-04-01T16:06:58","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/specification-mining-new-formalisms-algorithms-and-applications\/"},"modified":"2016-07-15T15:16:20","modified_gmt":"2016-07-15T22:16:20","slug":"specification-mining-new-formalisms-algorithms-and-applications","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/specification-mining-new-formalisms-algorithms-and-applications\/","title":{"rendered":"Specification Mining: New Formalisms, Algorithms and Applications"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. These tasks require understanding precisely a design&#8217;s  intended behavior, and thus are only effective if the specification is created right. However, it is extremely difficult to manually create a complete suite of good-quality formal specifications. Many real-world experiences indicate that poor or the lack of sufficient specifications can easily lead to misses of critical bugs.<\/p>\n<p>This talk presents research that seeks to mitigate the manual and error-prone process of creating formal specifications through automation. The overarching theme is specification mining &#8211; the process of inferring likely specifications. We present a collection of novel formalisms and techniques that are tailored for a variety of different applications. We study two topics at large &#8211; verification and synthesis. In verification, we show that relevant and meaningful specifications  can be mined dynamically from traces of a design, and are useful also for bug localization. In synthesis, we study the problem of synthesis from temporal logic specifications and focus on the problem of finding environment assumptions. We show that, by analyzing the counterstrategy of an unrealizable specification, we can systematically generate candidate environment assumptions that guide the specification towards realizability. In addition, this counterstrategy-guided  synthesis approach enables the automatic construction of a new class of semi-autonomous controller, called human-in-the-loop controllers. Further, we highlight efforts on incorporating Natural Language Processing techniques to make this technology more accessible to non-expert  users of formal methods.<\/p>\n<p>We conclude the talk by reviewing our efforts on tackling the general problem of model construction and specification creation, and discussing their increasing relevance in the emerging world of cyber-physical systems.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. These tasks require understanding precisely a design&#8217;s intended behavior, and thus are only effective if the specification is created right. However, it is extremely difficult to manually create a complete suite of good-quality formal specifications. Many real-world experiences indicate [&hellip;]<\/p>\n","protected":false},"featured_media":198269,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[],"msr-video-type":[],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-190707","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/ykLU8iE6aE8","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/190707"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/190707\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/198269"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=190707"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=190707"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=190707"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=190707"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=190707"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=190707"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}