{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:24Z","timestamp":1784211264453,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>In syntax-guided synthesis, one of the challenges is to reduce the enormous size of the search space. We observe that most search spaces are not just flat sets of programs, but can be endowed with a structure that we call an oriented metric. Oriented metrics measure the distance between programs, like ordinary metrics do, but are designed for settings in which operations have an orientation. Our focus is on the string and the bitvector domains, where operations like concatenation and bitwise conjunction transform an input into an output in a way that is not symmetric. We develop several new oriented metrics for these domains.<\/jats:p>\n                  <jats:p>Oriented metrics are designed for search space reduction, and we present four techniques: (i) pruning the search space to a ball around the ground truth, (ii) factorizing the search space by an equivalence that is induced by the oriented metric, (iii) abstracting the oriented metric (and hence the equivalence) and refining it, and (iv) improving the enumeration order by learning from abstract information. We acknowledge that these techniques are inspired by developments in the literature. By understanding their roots in oriented metrics, we can substantially increase their applicability and efficiency. We have integrated these techniques into a new synthesis algorithm and implemented the algorithm in a new solver. Notably, our solver is generic in the oriented metric over which it computes. We conducted experiments in the string and the bitvector domains, and consistently improve the performance over the state-of-the-art by more than an order of magnitude.<\/jats:p>","DOI":"10.1145\/3776717","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2174-2203","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Oriented Metrics for Bottom-Up Enumerative Synthesis"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8177-4675","authenticated-orcid":false,"given":"Jakob","family":"Tepe","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Arjun Radhakrishna and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer.10205 TACAS (2017) 319-336. doi:10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_3_2_5_2","unstructured":"Matej Balog Alexander L . Gaunt Marc Brockschmidt Sebastian Nowozin and Daniel Tarlow 2017.DeepCoder: Learning to Write Programs . In 5th International Conference on Learning Representations ICLR 2017 Toulon France April 24-26 2017 Conference Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=ByldLrql"},{"key":"e_1_3_2_6_2","unstructured":"Shraddha Barke Emmanuel Anaya Gonzalez Saketh Ram Kasibatla Taylor Berg-Kirkpatrick and Nadia Polikarpova 2024 HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis. In NeurIPS 2024 Vancouver BC Canada December 10 - 15 2024 Amir Globersons Lester Mackey Danielle Belgrave Angela Fan Ulrich Paquet Jakub M . Tomczak and Cheng Zhang (Eds.) http:\/\/papers.nips.cc\/paper_files\/paper\/2024\/hash\/1c9c85bae6161d52182d0fe2f3640512-Abstract-Conference.html"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Shraddha Barke Hila Peleg and Nadia Polikarpova. 2020. Just-in-time learning for bottom-up enumerative synthesis.Proc. ACM Program. Lang. 4 OOPSLA (2020) 227:1-227:29. doi:10.1145\/3428295","DOI":"10.1145\/3428295"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh UK) A. Gupta andD Kroening (Eds.)","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_2_9_2","first-page":"643","volume-title":"26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, Engin Kirda andThomas Ristenpart (Eds.) USENIX Association, 643-659. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/blazytko"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571226"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_7"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656447"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Robin David Luigi Coniglio and Mariano Ceccato 2020 QSynth - A Program Synthesis based approach for Binary Code Deobfuscation. In Binary Analysis Workshop (BAR) 2020. doi10.14722\/bar.2020.23009","DOI":"10.14722\/bar.2020.23009"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632913"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729336"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_13"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622830"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591285"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_3_2_27_2","volume-title":"Hacker's Delight, Second Edition","author":"Warren Jr Henry S.","year":"2013","unstructured":"Henry S. Warren Jr 2013 Hacker's Delight, Second Edition.Pearson Education. http:\/\/www.hackersdelight.org\/"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_3_2_30_2","first-page":"707","article-title":"Binary Codes Capable of Correcting Deletions, Insertions and Reversals","author":"Levenshtein V. I.","year":"1966","unstructured":"V. I. Levenshtein 1966 Binary Codes Capable of Correcting Deletions, Insertions and Reversals.Soviet Physics Doklady10 (Feb. 1966), 707","journal-title":"Soviet Physics Doklady"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Qikang Liu Yang He Yanwen Cai Byeongguk Kwak and Yuepeng Wang 2025 Synthesizing Document Database Queries Using Collection Abstractions . In ICSE 2025. IEEE Computer Society Los Alamitos CA USA 476-488. doi:10.1109\/ICSE55347.2025.00152","DOI":"10.1109\/ICSE55347.2025.00152"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Roland Meyerand Jakob Tepe 2025 Artifact for \"Oriented Metrics for Bottom-Up Enumerative Synthesis\". Zenodo. doi:10.5281\/zenodo.17345358","DOI":"10.5281\/zenodo.17345358"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Roland Meyer and Jakob Tepe2025 Oriented Metrics for Bottom-Up Enumerative Synthesis.CoRR abs\/2511.02491 (2025). doi:10.48550\/arXiv.2511.02491 arXiv:2511.02491","DOI":"10.48550\/arXiv.2511.02491"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.2"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594297"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Klaus U. Schulz and Stoyan Mihov. 2002 Fast string correction with Levenshtein automata. Int. J. Document Anal. Recognit. 5 1 (2002) 67-85. doi:10.1145\/3290386","DOI":"10.1145\/3290386"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6290-9"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_22"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_3_2_49_2","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\/pdf\/10.1145\/3776717","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:43:16Z","timestamp":1784209396000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776717"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776717"],"URL":"https:\/\/doi.org\/10.1145\/3776717","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}