We present a new approach to example-guided program synthesis based on counterexample-guided abstraction\u00a0refinement. Our method uses the abstract semantics of the underlying DSL to find a program P whose abstract\u00a0behavior satisfies the examples. However, since program P may be spurious with respect to the concrete\u00a0semantics, our approach iteratively refines the abstraction until we either find a program that satisfies the\u00a0examples or prove that no such DSL program exists. Because many programs have the same input-output\u00a0behavior in terms of their abstract semantics, this synthesis methodology significantly reduces the search\u00a0space compared to existing techniques that use purely concrete semantics.<\/p>\n
While synthesis using abstraction refinement (SYNGAR) could be implemented in different settings, we propose\u00a0a refinement-based synthesis algorithm that uses abstract finite tree automata (AFTA). Our technique uses\u00a0a coarse initial program abstraction to construct an initial AFTA, which is iteratively refined by constructing a\u00a0proof of incorrectness of any spurious program. In addition to ruling out the spurious program accepted by the\u00a0previous AFTA, proofs of incorrectness are also useful for ruling out many other spurious programs.<\/p>\n
We implement these ideas in a framework called Blaze, which can be instantiated in different domains\u00a0by providing a suitable DSL and its corresponding concrete and abstract semantics. We have used the Blaze\u00a0framework to build synthesizers for string and matrix transformations, and we compare Blaze with existing\u00a0techniques. Our results for the string domain show that Blaze compares favorably with FlashFill, a domain-specific synthesizer that is now deployed in Microsoft PowerShell. In the context of matrix manipulations, we\u00a0compare Blaze against Prose, a state-of-the-art general-purpose VSA-based synthesizer, and show that Blaze\u00a0results in a 90x speed-up over Prose. In both application domains, Blaze also consistently improves upon the\u00a0performance of two other existing techniques by at least an order of magnitude.<\/p>\n","protected":false},"excerpt":{"rendered":"
We present a new approach to example-guided program synthesis based on counterexample-guided abstraction\u00a0refinement. Our method uses the abstract semantics of the underlying DSL to find a program P whose abstract\u00a0behavior satisfies the examples. However, since program P may be spurious with respect to the concrete\u00a0semantics, our approach iteratively refines the abstraction until we either find […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193716],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-445569","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"ACM","msr_edition":"Principles of Programming Languages 2018 (POPL 2018)","msr_affiliation":"","msr_published_date":"2018-01-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"63:1-30","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"445572","msr_publicationurl":"","msr_doi":"https:\/\/doi.org\/10.1145\/3158151","msr_publication_uploader":[{"type":"file","title":"syngar_popl18","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/12\/syngar_popl18.pdf","id":445572,"label_id":0},{"type":"doi","title":"https:\/\/doi.org\/10.1145\/3158151","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_attachments":[],"msr-author-ordering":[{"type":"text","value":"Xinyu Wang","user_id":0,"rest_url":false},{"type":"text","value":"Isil Dillig","user_id":0,"rest_url":false},{"type":"user_nicename","value":"risin","user_id":33413,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=risin"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[444528],"msr_group":[],"msr_project":[],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/445569"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/445569\/revisions"}],"predecessor-version":[{"id":445578,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/445569\/revisions\/445578"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=445569"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=445569"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=445569"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=445569"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=445569"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=445569"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=445569"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=445569"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=445569"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=445569"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=445569"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=445569"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=445569"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=445569"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=445569"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}