{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T08:22:13Z","timestamp":1782289333658,"version":"3.54.5"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889,N00014-19-1-2318"],"award-info":[{"award-number":["N00014-17-1-2889,N00014-19-1-2318"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1420866, 1763871,1750965"],"award-info":[{"award-number":["1420866, 1763871,1750965"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to SyGuS problems (i.e., over expressions), synthesis problems over an imperative programming language, and synthesis problems over regular expressions.<\/jats:p>","DOI":"10.1145\/3434311","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Semantics-guided synthesis"],"prefix":"10.1145","volume":"5","author":[{"given":"Jinwoo","family":"Kim","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qinheping","family":"Hu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"1","article-title":"Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013. IEEE, 1-8.","journal-title":"IEEE"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Dana Fisman Rishabh Singh and Armando Solar-Lezama. 2017a. Sygus-comp 2017 : Results and analysis. arXiv preprint arXiv:1711.11438 ( 2017 ).","DOI":"10.4204\/EPTCS.260.9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_13"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"John K Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing data structure transformations from input-output examples. ACM SIGPLAN Notices 50 6 ( 2015 ) 229-239.","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating string processing in spreadsheets using input-output examples. ACM Sigplan Notices 46 1 ( 2011 ) 317-330.","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_21"},{"key":"e_1_2_1_14_1","unstructured":"S.C. Johnson. 1975. YACC: Yet Another Compiler-Compiler. Technical Report Comp. Sci. Tech. Rep. 32. Bell Laboratories."},{"key":"e_1_2_1_15_1","volume-title":"Semantics-Guided Synthesis. arXiv preprint arXiv","author":"Kim Jinwoo","year":"2008","unstructured":"Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps. 2020. Semantics-Guided Synthesis. arXiv preprint arXiv: 2008. 09836 ( 2020 )."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Anvesh Komuravelli Arie Gurfinkel and Sagar Chaki. 2016. SMT-based model checking for recursive programs. Formal Methods in System Design 48 3 ( 2016 ) 175-205.","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_2_1_17_1","unstructured":"N. Lavra\u010d and S. D\u017eeroski. 1994. Inductive Logic Programming: Techniques and Applications. Ellis Horwood."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993236.2993244"},{"key":"e_1_2_1_19_1","unstructured":"Kenneth L McMillan and Andrey Rybalchenko. 2013. Solving constrained Horn clauses using interpolation. Tech. Rep. MSR-TR-2013-6 ( 2013 )."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"S. Muggleton. 1991. Inductive logic programming. New Generation Comp. 8 4 ( 1991 ) 295-317.","DOI":"10.1007\/BF03037089"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360565"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304059"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"J.R. Quinlan. 1990. Learning logical definitions from Relations. Mach. Learn. 5 ( 1990 ) 239-266.","DOI":"10.1007\/BF00117105"},{"key":"e_1_2_1_25_1","volume-title":"CVC4SY for SyGuS-COMP","author":"Reynolds Andrew","year":"2019","unstructured":"Andrew Reynolds, Haniel Barbosa, Andres N\u00f6tzli, Clark Barrett, and Cesare Tinelli. 2019. CVC4SY for SyGuS-COMP 2019. arXiv preprint arXiv: 1907. 10175 ( 2019 )."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_18"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_1_30_1","volume-title":"Learning Abstractions for Program Synthesis. In International Conference on Computer Aided Verification. Springer, 407-426","author":"Wang Xinyu","year":"2018","unstructured":"Xinyu Wang, Greg Anderson, Isil Dillig, and Kenneth L McMillan. 2018a. Learning Abstractions for Program Synthesis. In International Conference on Computer Aided Verification. Springer, 407-426."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL ( 2017 ), 1-30","author":"Wang Xinyu","year":"2017","unstructured":"Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017. Program synthesis using abstraction refinement. Proceedings of the ACM on Programming Languages 2, POPL ( 2017 ), 1-30."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Xinyu Wang Isil Dillig and Rishabh Singh. 2018b. Program Synthesis Using Abstraction Refinement. PACMPL 2 POPL ( 2018 ) 63 : 1-63 : 30.","DOI":"10.1145\/3158151"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434311","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434311","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:08Z","timestamp":1781853908000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434311"],"URL":"https:\/\/doi.org\/10.1145\/3434311","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}