{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T15:40:33Z","timestamp":1782834033416,"version":"3.54.5"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1837023,2046071,2319425"],"award-info":[{"award-number":["1837023,2046071,2319425"]}],"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":[[2024,1,2]]},"abstract":"<jats:p>\n            Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our S\n            <jats:sc>y<\/jats:sc>\n            G\n            <jats:sc>u<\/jats:sc>\n            S solver D\n            <jats:sc>ryad<\/jats:sc>\n            S\n            <jats:sc>ynth<\/jats:sc>\n            , which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, D\n            <jats:sc>ryad<\/jats:sc>\n            S\n            <jats:sc>ynth<\/jats:sc>\n            successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker\u2019s Delight problems.\n          <\/jats:p>","DOI":"10.1145\/3632913","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2129-2159","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9941-6394","authenticated-orcid":false,"given":"Yuantian","family":"Ding","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9476-7349","authenticated-orcid":false,"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","first-page":"934","DOI":"10.1007\/978-3-642-39799-8_67","volume-title":"Computer Aided Verification","author":"Albarghouthi Aws","year":"2013","unstructured":"Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 934\u2013950."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"e_1_3_1_4_1","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alur Rajeev","year":"2017","unstructured":"Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 319\u2013336."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_1_6_1","unstructured":"Matej Balog Alexander L. Gaunt Marc Brockschmidt Sebastian Nowozin and Daniel Tarlow. 2017. DeepCoder: Learning to Write Programs. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=ByldLrqlx"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428295"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_9_1","volume-title":"The SMT-LIB Standard: Version 2.6","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571226"},{"key":"e_1_3_1_11_1","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/978-3-030-53291-8_30","volume-title":"Computer Aided Verification","author":"Chen Yanju","year":"2020","unstructured":"Yanju Chen, Chenglong Wang, Osbert Bastani, Isil Dillig, and Yu Feng. 2020. Program Synthesis Using Deduction-Guided Reinforcement Learning. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 587\u2013610."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10129930"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_1_16_1","unstructured":"Glenn Fowler Landon Curt Noll and Phong Vo. 1991. Fowler-Noll-Vo (FNV) Hash Function. Fowler-Noll-Vo Website. http:\/\/www.isthe.com\/chongo\/tech\/comp\/fnv\/"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exr021"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386027"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/978-3-319-21668-3_22","volume-title":"Computer Aided Verification","author":"Jeon Jinseong","year":"2015","unstructured":"Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, and Jeffrey S. Foster. 2015. Adaptive Concretization for Parallel Program Synthesis. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham, 377\u2013394."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0269-8"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485544"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_3_1_27_1","article-title":"Neural Sketch Learning for Conditional Program Generation","author":"Murali Vijayaraghavan","year":"2018","unstructured":"Vijayaraghavan Murali, Letao Qi, Swarat Chaudhuri, and Chris Jermaine. 2018. Neural Sketch Learning for Conditional Program Generation. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HkfXMz-Ab","journal-title":"International Conference on Learning Representations"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485496"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_29"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_3_1_31_1","unstructured":"OpenAI. 2022. ChatGPT: Large-scale Language Models for Conversational AI. OpenAI Website. https:\/\/openai.com\/research\/chatgpt"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022643204877"},{"key":"e_1_3_1_36_1","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"Reynolds Andrew","year":"2019","unstructured":"Andrew Reynolds, Haniel Barbosa, Andres N\u00f6tzli, Clark Barrett, and Cesare Tinelli. 2019. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 74\u201383."},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"Reynolds Andrew","year":"2015","unstructured":"Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham, 198\u2013216."},{"key":"e_1_3_1_38_1","article-title":"Learning a Meta-Solver for Syntax-Guided Program Synthesis","author":"Si Xujie","year":"2019","unstructured":"Xujie Si, Yuan Yang, Hanjun Dai, Mayur Naik, and Le Song. 2019. Learning a Meta-Solver for Syntax-Guided Program Synthesis. In International Conference on Learning Representations. OpenReview. https:\/\/openreview.net\/forum?id=Syl8Sn0cK7","journal-title":"International Conference on Learning Representations"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_3_1_42_1","author":"Warren Henry S.","year":"2012","unstructured":"Henry S. Jr. Warren. 2012. Hacker\u2019s Delight (2 ed.). Addison-Wesley Professional.","journal-title":"Hacker\u2019s Delight"},{"key":"e_1_3_1_43_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\/3632913","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632913","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632913","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:58Z","timestamp":1751659618000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632913"],"URL":"https:\/\/doi.org\/10.1145\/3632913","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}