{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:16:54Z","timestamp":1783009014869,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100014718","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1837023"],"award-info":[{"award-number":["CCF-1837023"]}],"id":[{"id":"10.13039\/100014718","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3386027","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"1159-1174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Reconciling enumerative and deductive program synthesis"],"prefix":"10.1145","author":[{"given":"Kangjing","family":"Huang","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peiyuan","family":"Shen","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanjun","family":"Wang","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"FMCAD 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntaxguided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. 1\u20138. http:\/\/ieeexplore. ieee.org\/document\/6679385\/"},{"key":"e_1_3_2_2_2_1","volume-title":"CAV (2) (Lecture Notes in Computer Science)","author":"Alur Rajeev","unstructured":"Rajeev Alur, Pavol Cern\u00fd, and Arjun Radhakrishna. 2015. Synthesis Through Unification. In CAV (2) (Lecture Notes in Computer Science), Vol. 9207. Springer, 163\u2013179."},{"key":"e_1_3_2_2_3_1","volume-title":"SyGuS-Comp 2018: Results and Analysis. https:\/\/sygus.org\/comp\/2018\/report.pdf","author":"Alur Rajeev","year":"2018","unstructured":"Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Armando Solar-Lezama. 2018. SyGuS-Comp 2018: Results and Analysis. https:\/\/sygus.org\/comp\/2018\/report.pdf (2018)."},{"key":"e_1_3_2_2_4_1","unstructured":"Rajeev Alur Dana Fisman Rishabh Singh and Armando Solar-Lezama. 2016."},{"key":"e_1_3_2_2_5_1","volume-title":"Results and Analysis. https:\/\/arxiv.org\/abs\/1611.07627","author":"Comp","year":"2016","unstructured":"SyGuS-Comp 2016: Results and Analysis. https:\/\/arxiv.org\/abs\/1611.07627 (2016). arXiv: 1611.07627"},{"key":"e_1_3_2_2_6_1","volume-title":"SyGuS-Comp 2017: Results and Analysis. (11","author":"Alur Rajeev","year":"2017","unstructured":"Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. 2017. SyGuS-Comp 2017: Results and Analysis. (11 2017). arXiv: 1711.11438 https:\/\/arxiv.org\/abs\/1711.11438"},{"key":"e_1_3_2_2_7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Alur Rajeev","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_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_2_2_9_1","volume-title":"DeepCoder: Learning to Write Programs. CoRR abs\/1611.01989","author":"Balog Matej","year":"2016","unstructured":"Matej Balog, Alexander L. Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2016. DeepCoder: Learning to Write Programs. CoRR abs\/1611.01989 (2016). arXiv: 1611.01989 http: \/\/arxiv.org\/abs\/1611.01989"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_3_2_2_11_1","volume-title":"What\u2019s Decidable about Syntax-Guided Synthesis? (10","author":"Caulfield Benjamin","year":"2015","unstructured":"Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia, and Stavros Tripakis. 2015. What\u2019s Decidable about Syntax-Guided Synthesis? (10 2015). arXiv: 1510.08393 https:\/\/arxiv.org\/abs\/1510.08393"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_13_1","volume-title":"Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In POPL\u201915. ACM, 689\u2013700.","author":"Delaware Benjamin","year":"2015","unstructured":"Benjamin Delaware, Clement Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In POPL\u201915. ACM, 689\u2013700."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_13"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"crossref","unstructured":"John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-output Examples. In PLDI\u201915 (Portland OR USA). ACM 229\u2013239.","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211346.3211355"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240260"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_22"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0269-8"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_3_2_2_28_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A","author":"Li Boyang","unstructured":"Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, and Mooly Sagiv. 2013. Synthesis of Circular Compositional Program Proofs via Abduction. In Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A. Smolka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 370\u2013384."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234198"},{"key":"e_1_3_2_2_30_1","volume-title":"Bayesian Sketch Learning for Program Synthesis. CoRR abs\/1703.05698","author":"Murali Vijayaraghavan","year":"2017","unstructured":"Vijayaraghavan Murali, Swarat Chaudhuri, and Chris Jermaine. 2017. Bayesian Sketch Learning for Program Synthesis. CoRR abs\/1703.05698 (2017). arXiv: 1703.05698 http:\/\/arxiv.org\/abs\/1703.05698"},{"key":"e_1_3_2_2_31_1","volume-title":"Data-Driven Loop Invariant Inference with Automatic Feature Synthesis. (07","author":"Padhi Saswat","year":"2017","unstructured":"Saswat Padhi and Todd Millstein. 2017. Data-Driven Loop Invariant Inference with Automatic Feature Synthesis. (07 2017). arXiv: 1707.02029 https:\/\/arxiv.org\/abs\/1707.02029"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.840306"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_26"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_3_2_2_40_1","unstructured":"2594302"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_2_43_1","unstructured":"Armando Solar-Lezama. 2016. The Sketch Programmers Manual. Version 1.7.2."},{"key":"e_1_3_2_2_44_1","unstructured":"Armando Solar-Lezama. 2018. Introduction to Program Synthesis. https:\/\/people.csail.mit.edu\/asolar\/SynthesisCourse\/TOC.htm"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. In ASPLOS\u201906 (San Jose California USA). ACM 404\u2013415.","DOI":"10.1145\/1168918.1168907"},{"key":"e_1_3_2_2_46_1","volume-title":"Foster","author":"Srivastava Saurabh","year":"2010","unstructured":"Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From Program Verification to Program Synthesis. In POPL\u201910 (Madrid, Spain). ACM, 313\u2013326."},{"key":"e_1_3_2_2_47_1","volume-title":"StarExec: A Cross-Community Infrastructure for Logic Solving","author":"Stump Aaron","unstructured":"Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. 2014. StarExec: A Cross-Community Infrastructure for Logic Solving. In Automated Reasoning, St\u00e9phane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.). Springer International Publishing, Cham, 367\u2013373."},{"key":"e_1_3_2_2_48_1","volume-title":"TRANSIT: Specifying Protocols with Concolic Snippets. In PLDI. 287\u2013296.","author":"Udupa Abhishek","year":"2013","unstructured":"Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M.K. Martin, and Rajeev Alur. 2013. TRANSIT: Specifying Protocols with Concolic Snippets. In PLDI. 287\u2013296."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Martin Vechev and Eran Yahav. 2008. Deriving Linearizable Finegrained Concurrent Objects. In PLDI\u201908. ACM 125\u2013135.","DOI":"10.1145\/1375581.1375598"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386027","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:49Z","timestamp":1750199929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":48,"alternative-id":["10.1145\/3385412.3386027","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3386027","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}