{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:20:49Z","timestamp":1770286849535,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Program synthesis is now a reality, and we are approaching the point where domain-specific synthesizers can now handle problems of practical sizes. Moreover, some of these tools are finding adoption in industry. However, for synthesis to become a mainstream technique adopted at large by programmers as well as by end-users, we need to design programmable synthesis frameworks that (<jats:italic>i<\/jats:italic>)\u00a0are not tailored to specific domains or languages, (<jats:italic>ii<\/jats:italic>)\u00a0enable one to specify synthesis problems with a variety of qualitative and quantitative objectives in mind, and (<jats:italic>iii<\/jats:italic>)\u00a0come equipped with theoretical as well as practical guarantees. We report on our work on designing such frameworks and on building synthesis engines that can handle program-synthesis problems describable in such frameworks, and describe open challenges and opportunities.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_4","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"84-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Programmable Program Synthesis"],"prefix":"10.1007","author":[{"given":"Loris","family":"D\u2019Antoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qinheping","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinwoo","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part I. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"4_CR3","unstructured":"Amodio, M., Chaudhuri, S., Reps, T.W.: Neural attribute machines for program generation. CoRR, abs\/1705.09231 (2017)"},{"issue":"OOPSLA,","key":"4_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428295","volume":"4","author":"S Barke","year":"2020","unstructured":"Barke, S., Peleg, H., Polikarpova, N.: Just-in-time learning for bottom-up enumerative synthesis. Proc. ACM Program. Lang. 4(OOPSLA,), 1\u201329 (2020)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR5","unstructured":"Comon, H., et al.: Tree automata techniques and applications (2007). http:\/\/www.grappa.univ-lille3.fr\/tata. Accessed 12 October 2007"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-41540-6_21","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2016","unstructured":"D\u2019Antoni, L., Samanta, R., Singh, R.: Qlose: program repair with quantitative objectives. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 383\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_21"},{"key":"4_CR7","unstructured":"ESolver. https:\/\/github.com\/abhishekudupa\/sygus-comp14"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Feldman, M.Q., Wang, Y., Byrd, W.E., Guimbreti\u00e8re, F., Andersen, E.: Towards answering \u201cAm I on the right track?\u201d Automatically using program synthesis. In Proceedings of the 2019 ACM SIGPLAN Symposium on SPLASH-E, SPLASH-E 2019, pp. 13\u201324, New York, NY, USA. Association for Computing Machinery (2019)","DOI":"10.1145\/3358711.3361626"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: PPDP (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-319-40229-1_2","volume-title":"Automated Reasoning","author":"S Gulwani","year":"2016","unstructured":"Gulwani, S.: Programming by examples: applications, algorithms, and ambiguity resolution. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 9\u201314. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_2"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Hu, Q., Cyphert, J., D\u2019Antoni, L., Reps, T.: Synthesis with asymptotic resource bounds. In: CAV (2021)","DOI":"10.1007\/978-3-030-81685-8_37"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-96145-3_21","volume-title":"Computer Aided Verification","author":"Q Hu","year":"2018","unstructured":"Hu, Q., D\u2019Antoni, L.: Syntax-guided synthesis with quantitative syntactic objectives. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 386\u2013403. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_21"},{"key":"4_CR13","unstructured":"Johnson, S.: YACC: Yet another compiler-compiler. Technical Report Computer Science Technical report 32, Bell Laboratories (1975)"},{"issue":"POPL","key":"4_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434311","volume":"5","author":"J Kim","year":"2021","unstructured":"Kim, J., Hu, Q., D\u2019Antoni, L., Reps, T.: Semantics-guided synthesis. Proc. ACM on Program. Lang. 5(POPL), 1\u201332 (2021)","journal-title":"Proc. ACM on Program. Lang."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.:. Resource-guided program synthesis. In: PLDI, pp. 253\u2013268 (2019)","DOI":"10.1145\/3314221.3314602"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-guided program synthesis. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 253\u2013268 (2019)","DOI":"10.1145\/3314221.3314602"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sekiyama, T., Sato, I., Unno, H.: Toward neural-network-guided program synthesis and verification. CoRR, abs\/2103.09414 (2021)","DOI":"10.1007\/978-3-030-88806-0_12"},{"issue":"3","key":"4_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-662-21545-6_18","volume-title":"Automata, Languages and Programming","author":"B Lang","year":"1974","unstructured":"Lang, B.: Deterministic techniques for efficient non-deterministic parsers. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 255\u2013269. Springer, Heidelberg (1974). https:\/\/doi.org\/10.1007\/978-3-662-21545-6_18"},{"key":"4_CR20","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California, March (2004)"},{"issue":"POPL","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434335","volume":"5","author":"W Lee","year":"2021","unstructured":"Lee, W.: Combining the top-down propagation and bottom-up enumeration for inductive program synthesis. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208\u2013217 (2015)","DOI":"10.1145\/2737924.2737982"},{"issue":"OOPSLA","key":"4_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3360565","volume":"3","author":"R Pan","year":"2019","unstructured":"Pan, R., Hu, Q., Xu, G., D\u2019Antoni, L.: Automatic repair of regular expressions. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201329 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 522\u2013538 (2016)","DOI":"10.1145\/2908080.2908093"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, 25\u201330 October 2015, pp. 107\u2013126 (2015)","DOI":"10.1145\/2858965.2814310"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part II. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2012","unstructured":"Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf. 15, 475\u2013495 (2012). https:\/\/doi.org\/10.1007\/s10009-012-0249-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, pp. 135\u2013152 (2013)","DOI":"10.1145\/2509578.2509586"},{"issue":"POPL","key":"4_CR29","first-page":"63:1","volume":"2","author":"X Wang","year":"2018","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. PACMPL 2(POPL), 63:1-63:30 (2018)","journal-title":"PACMPL"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:41:19Z","timestamp":1672857679000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}