{"id":678045,"date":"2020-07-23T13:09:00","date_gmt":"2020-07-23T20:09:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=678045"},"modified":"2020-07-23T16:30:31","modified_gmt":"2020-07-23T23:30:31","slug":"synthesis-through-unification","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/synthesis-through-unification\/","title":{"rendered":"Synthesis Through Unification"},"content":{"rendered":"

Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S<\/em> of inputs and a candidate program P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span> that is correct for S<\/em>. The synthesizer repeatedly checks if there exists a counterexample input c<\/em> such that the execution of P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span> is incorrect on c<\/em>. If so, the synthesizer enlarges S<\/em> to include c<\/em>, and picks a program from the program space that is correct for the new set S<\/em>.<\/p>\n

The STUN approach extends CEGIS with the idea that given a program P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span> that is correct for a subset of inputs, the synthesizer can try to find a program P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow>\u2032<\/mo><\/msup><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span> that is correct for the rest of the inputs. If P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span> and P<\/mi>r<\/mi>o<\/mi>g<\/mi><\/mrow>\u2032<\/mo><\/msup><\/math>\">P<\/span>r<\/span>o<\/span>g<\/span><\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span> can be unified<\/em> into a program in the program space, then a solution has been found. We present a generic synthesis procedure based on the STUN approach and specialize it for three different domains by providing the appropriate unification operators. We implemented these specializations in prototype tools, and we show that our tools often performs significantly better on standard benchmarks than a tool based on a pure CEGIS approach.<\/p>\n","protected":false},"excerpt":{"rendered":"

Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs […]<\/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":""},"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-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-678045","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"","msr_edition":"","msr_affiliation":"","msr_published_date":"2015-7-1","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","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":0,"msr_main_download":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/07\/cav15a.pdf","id":"677982","title":"cav15a","label_id":"243132","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/link.springer.com\/chapter\/10.1007%2F978-3-319-21668-3_10","label_id":"243109","label":0},{"type":"doi","viewUrl":"false","id":"false","title":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_10","label_id":"243106","label":0}],"msr_related_uploader":"","msr_attachments":[],"msr-author-ordering":[{"type":"text","value":"Rajeev Alur","user_id":0,"rest_url":false},{"type":"text","value":"Pavol Cerny","user_id":0,"rest_url":false},{"type":"user_nicename","value":"Arjun Radhakrishna","user_id":39405,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Arjun Radhakrishna"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[678288],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":678288,"post_title":"Divide-and-Conquer Algorithms for Synthesis","post_name":"divide-and-conquer-algorithms-for-synthesis","post_type":"msr-project","post_date":"2020-07-23 15:09:39","post_modified":"2020-07-24 09:32:09","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/divide-and-conquer-algorithms-for-synthesis\/","post_excerpt":"This project aims to produce more efficient algorithms for program synthesis using techniques that decompose the task at hand into simpler tasks. Here, instances of the program synthesis problem are solved by finding smaller sub-solutions that are correct for subsets of the input space and then recombining them into a full correct solution. The tool EUSolver which was the outcome of this project won the general track at the Syntax Guided Synthesis (SyGuS) competitions in…","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/678288"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/678045"}],"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\/678045\/revisions"}],"predecessor-version":[{"id":678051,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/678045\/revisions\/678051"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=678045"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=678045"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=678045"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=678045"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=678045"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=678045"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=678045"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=678045"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=678045"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=678045"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=678045"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=678045"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=678045"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=678045"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=678045"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=678045"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}