{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T02:28:32Z","timestamp":1789180112911,"version":"build-2803163510"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DARPA and Air Force","award":["FA8750-20-C-0002"],"award-info":[{"award-number":["FA8750-20-C-0002"]}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA8750-20-C-0208"],"award-info":[{"award-number":["FA8750-20-C-0208"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1762299, 1811865, 1918651"],"award-info":[{"award-number":["1762299, 1811865, 1918651"]}],"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":[[2022,1,16]]},"abstract":"<jats:p>We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 94% of the benchmarks in our benchmark suite, outperforming prior work.<\/jats:p>","DOI":"10.1145\/3498682","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Bottom-up synthesis of recursive functional programs using angelic execution"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8338-4008","authenticated-orcid":false,"given":"Anders","family":"Miltner","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5658-9956","authenticated-orcid":false,"given":"Adrian Trejo","family":"Nu\u00f1ez","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6188-9980","authenticated-orcid":false,"given":"Ana","family":"Brendel","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6859-1391","authenticated-orcid":false,"given":"Swarat","family":"Chaudhuri","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737952"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10828-9_61"},{"key":"e_1_2_2_5_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree Automata Techniques and Applications. https:\/\/hal.inria.fr\/hal-03367725  Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree Automata Techniques and Applications. https:\/\/hal.inria.fr\/hal-03367725"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837629"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386027"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_2_2_13_1","article-title":"Inductive synthesis of functional programs: An explanation based generalization approach","volume":"7","author":"Kitzelmann Emanuel","year":"2006","unstructured":"Emanuel Kitzelmann , Ute Schmid , Roland Olsson , and Leslie Pack Kaelbling . 2006 . Inductive synthesis of functional programs: An explanation based generalization approach . Journal of Machine Learning Research , 7 , 2 (2006). Emanuel Kitzelmann, Ute Schmid, Roland Olsson, and Leslie Pack Kaelbling. 2006. Inductive synthesis of functional programs: An explanation based generalization approach. Journal of Machine Learning Research, 7, 2 (2006).","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/945645.945654"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594333"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786811"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408991"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2011.428"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_2_2_22_1","volume-title":"Ana Brendel, Swarat Chaudhuri, and Isil Dillig.","author":"Miltner Anders","year":"2021","unstructured":"Anders Miltner , Adrian Trejo Nu\u00f1ez , Ana Brendel, Swarat Chaudhuri, and Isil Dillig. 2021 . Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution . arxiv:2107.06253. Anders Miltner, Adrian Trejo Nu\u00f1ez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig. 2021. Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution. arxiv:2107.06253."},{"key":"e_1_2_2_23_1","volume-title":"BUSTLE: Bottom-up program-Synthesis Through Learning-guided Exploration. arXiv preprint arXiv:2007.14381.","author":"Odena Augustus","year":"2020","unstructured":"Augustus Odena , Kensen Shi , David Bieber , Rishabh Singh , and Charles Sutton . 2020 . BUSTLE: Bottom-up program-Synthesis Through Learning-guided Exploration. arXiv preprint arXiv:2007.14381. Augustus Odena, Kensen Shi, David Bieber, Rishabh Singh, and Charles Sutton. 2020. BUSTLE: Bottom-up program-Synthesis Through Learning-guided Exploration. arXiv preprint arXiv:2007.14381."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.44"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.322002"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276525"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498682","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498682","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498682"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498682"],"URL":"https:\/\/doi.org\/10.1145\/3498682","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}