{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:16:41Z","timestamp":1791299801125,"version":"4.1.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, can output on a given input. If the set does not contain the desired output, the partial program and all its possible completions can be pruned. In its general form, abstraction-based pruning requires manually designed, domain-specific abstract domains and semantics, and thus has only been used in domain-specific synthesizers.<\/jats:p>\n                  <jats:p>This paper provides sufficient conditions under which a form of abstraction-based pruning can be automated for arbitrary synthesis problems in the general-purpose Semantics-Guided Synthesis (SemGuS) framework without requiring manually-defined abstract domains. We show that if the semantics of the language for which we are synthesizing programs exhibits some monotonicity properties, one can obtain an abstract interval-based semantics for free from the concrete semantics of the programming language, and use such semantics to effectively prune the search space. We also identify a condition that ensures such abstract semantics can be used to compute a precise abstraction of the set of values that a program derivable from a given hole in a partial program can produce. These precise abstractions make abstraction-based pruning more effective.<\/jats:p>\n                  <jats:p>\n                    We implement our approach in a tool, M\n                    <jats:sc>oito<\/jats:sc>\n                    , which can tackle synthesis problems defined in the SemGuS framework. M\n                    <jats:sc>oito<\/jats:sc>\n                    can automate interval-based pruning without any a-priori knowledge of the problem domain, and solve synthesis problems that previously required domain-specific, abstraction-based synthesizers\u2014e.g., synthesis of regular expressions, CSV file schema, and imperative programs from examples.\n                  <\/jats:p>","DOI":"10.1145\/3689744","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"935-961","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3766-5204","authenticated-orcid":false,"given":"Keith J.C.","family":"Johnson","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0230-5185","authenticated-orcid":false,"given":"Rahul","family":"Krishnan","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.202.3"},{"key":"e_1_3_1_4_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Arjun Radhakrishna and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In International Conference on Tools and Algorithms for Construction and Analysis of Systems. https:\/\/api.semanticscholar.org\/CorpusID:9465894","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2010.09.003"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Center for High Throughput Computing. 2006. Center for High Throughput Computing. https:\/\/doi.org\/10.21231\/GNT1-HW21 10.21231\/GNT1-HW21","DOI":"10.21231\/GNT1-HW21"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03456-5_28"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591285"},{"key":"e_1_3_1_12_1","unstructured":"Keith J.C. Johnson Rahul Krishnan Thomas Reps and Loris D\u2019Antoni. 2024a. Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics. arXiv:2408.15822 [cs.PL] https:\/\/arxiv.org\/abs\/2408.15822"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Keith J.C. Johnson Rahul Krishnan Thomas Reps and Loris D\u2019Antoni. 2024b. Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics. https:\/\/doi.org\/10.5281\/zenodo.12669773 10.5281\/zenodo.12669773","DOI":"10.5281\/zenodo.12669773"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_2"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Pankaj Kumar Kalita Sujit Kumar Muduli Loris D\u2019Antoni Thomas Reps and Subhajit Roy. 2022. Synthesizing Abstract Transformers. arXiv:2105.00493 [cs.PL]","DOI":"10.1145\/3563334"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"Komuravelli Anvesh","year":"2014","unstructured":"Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 17\u201334."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993236.2993244"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632858"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645843.758268"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_1_23_1","unstructured":"Adam Retter David Underdown and Rob Walpole. 2016. CSV Schema Language 1.1. https:\/\/digital-preservation.github.io\/csv-schema\/csv-schema-1.1.html"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Tushar Sharma and Thomas Reps. 2017. Sound Bit-Precise Numerical Domains. 500\u2013520. https:\/\/doi.org\/10.1007\/978-3-319-52234-0_27 10.1007\/978-3-319-52234-0_27","DOI":"10.1007\/978-3-319-52234-0_27"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236034"},{"key":"e_1_3_1_26_1","unstructured":"Sunbeom So and Hakjoo Oh. 2017. Synthesizing Imperative Programs from Examples Guided by Static Analysis. arXiv:1702.06334 [cs.PL]"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2005.07.035"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706338"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-319-96145-3_22","volume-title":"Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I 30","author":"Wang Xinyu","year":"2018","unstructured":"Xinyu Wang, Greg Anderson, Isil Dillig, and Kenneth L McMillan. 2018. Learning Abstractions for Program Synthesis. In Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I 30. Springer, 407\u2013426."},{"key":"e_1_3_1_32_1","unstructured":"Xinyu Wang Isil Dillig and Rishabh Singh. 2017b. Program Synthesis using Abstraction Refinement. CoRR abs\/1710.07740 (2017). arXiv:1710.07740 http:\/\/arxiv.org\/abs\/1710.07740"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591288"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689744","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:09:40Z","timestamp":1770196180000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":32,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689744"],"URL":"https:\/\/doi.org\/10.1145\/3689744","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}