{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:06:32Z","timestamp":1770293192118,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"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>Quantifier bounding is a standard approach in inductive program synthesis in dealing with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis problem is specified by an input reference (recursive) function and a <jats:italic>recursion skeleton<\/jats:italic>. The goal is to synthesize a recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton. In this context, we illustrate that it is possible to <jats:italic>selectively<\/jats:italic> bound a <jats:italic>subset<\/jats:italic> of the (recursively typed) parameters, each by a suitable bound. The choices are guided by counterexamples. The evaluation of our strategy on a broad set of benchmarks shows that it succeeds in efficiently synthesizing non-trivial recursive functions where standard across-the-board bounding would fail.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_39","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"832-855","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Counterexample-Guided Partial Bounding for Recursive Function Synthesis"],"prefix":"10.1007","author":[{"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[]},{"given":"Victor","family":"Nicolet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"39_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-89719-6_7","volume-title":"Trends in Functional Programming","author":"O Abrahamsson","year":"2018","unstructured":"Abrahamsson, O., Myreen, M.O.: Automatically introducing tail recursion in\u00a0CakeML. In: Wang, M., Owens, S. (eds.) TFP 2017. LNCS, vol. 10788, pp. 118\u2013134. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89719-6_7"},{"key":"39_CR2","doi-asserted-by":"crossref","unstructured":"Ahmad, M.B.S., Cheung, A.: Automatically leveraging MapReduce frameworks for data-intensive applications. In: Proceedings of the 2018 International Conference on Management of Data, SIGMOD 2018. ACM (2018)","DOI":"10.1145\/3183713.3196891"},{"key":"39_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"934","DOI":"10.1007\/978-3-642-39799-8_67","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 934\u2013950. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67"},{"key":"39_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"39_CR6","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977)","journal-title":"J. ACM"},{"key":"39_CR7","unstructured":"Farzan, A., Nicolet, V.: Counterexample-guided partial bounding for recursive function synthesis (Extended Version). https:\/\/www.cs.toronto.edu\/~azadeh\/resources\/papers\/cav21-extended.pdf"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Farzan, A., Nicolet, V.: Synthesis of divide and conquer parallelism for loops. In: Proceedings of the 38th ACM Conference on Programming Language Design and Implementation, PLDI 2017 (2017)","DOI":"10.1145\/3062341.3062355"},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Ahmad, M.B.S., Bodik, R.: Gradual synthesis for static parallelization of single-pass array-processing programs. In: Proceedings of the 38th ACM Conference on Programming Language Design and Implementation, PLDI 2017 (2017)","DOI":"10.1145\/3062341.3062382"},{"key":"39_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-662-54577-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YMY Feldman","year":"2017","unstructured":"Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 76\u201395. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_5"},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM Conference on Programming Language Design and Implementation, PLDI 2015 (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: Proceedings of the 43rd ACM Symposium on Principles of Programming Languages, POPL 2016 (2016)","DOI":"10.1145\/2837614.2837629"},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"Hamilton, G.W., Jones, N.D.: Distillation with labelled transition systems. In: Proceedings of the ACM 2012 Workshop on Partial Evaluation and Program Manipulation, pp. 15\u201324. PEPM 2012. ACM (2012)","DOI":"10.1145\/2103746.2103753"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-662-54577-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JP Inala","year":"2017","unstructured":"Inala, J.P., Polikarpova, N., Qiu, X., Lerner, B.S., Solar-Lezama, A.: Synthesis of recursive ADT transformations from reusable templates. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 247\u2013263. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_14"},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., et al.: Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In: Proceedings of the 2016 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 145\u2013164. ACM (2016)","DOI":"10.1145\/2983990.2983993"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Katayama, S.: An analytical inductive functional programming system that avoids unintended programs. In: Proceedings of the 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012 (2012)","DOI":"10.1145\/2103746.2103758"},{"issue":"15","key":"39_CR17","first-page":"429","volume":"7","author":"E Kitzelmann","year":"2006","unstructured":"Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: an explanation based generalization approach. J. Mach. Learn. Res. 7(15), 429\u2013454 (2006)","journal-title":"J. Mach. Learn. Res."},{"key":"39_CR18","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013 (2013)","DOI":"10.1145\/2509136.2509555"},{"key":"39_CR19","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of the 36th ACM Symposium on Principles of Programming Languages, POPL 2009 (2009)","DOI":"10.1145\/1480881.1480933"},{"key":"39_CR20","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM Conference on Programming Language Design and Implementation, pp. 222\u2013233, PLDI 2011 (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"39_CR21","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of the 37th ACM Symposium on Principles of Programming Languages, POPL 2010 (2010)","DOI":"10.1145\/1706299.1706355"},{"key":"39_CR22","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml system release 4.11: Documentation and user\u2019s manual, p. 823 (2019)"},{"key":"39_CR23","doi-asserted-by":"crossref","unstructured":"Morihata, A., Matsuzaki, K.: Automatic parallelization of recursive functions using quantifier elimination. In: Proceedings of the 10th International Conference on Functional and Logic Programming, FLOPS 2010 (2010)","DOI":"10.1007\/978-3-642-12251-4_23"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"Morihata, A., Matsuzaki, K., Hu, Z., Takeichi, M.: The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer. In: Proceedings of the 36th ACM Symposium on Principles of Programming Languages, POPL 2009 (2009)","DOI":"10.1145\/1480881.1480905"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"39_CR26","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of the 38th ACM Symposium on Principles of Programming Languages, POPL 2011 (2011)","DOI":"10.1145\/1926385.1926453"},{"key":"39_CR27","doi-asserted-by":"crossref","unstructured":"Osera, P.M., Zdancewic, S.: Type-and-example-directed Program Synthesis. In: Proceedings of the 36th ACM Conference on Programming Language Design and Implementation, PLDI 2015 (2015)","DOI":"10.1145\/2737924.2738007"},{"key":"39_CR28","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM Conference on Programming Language Design and Implementation, PLDI 2016 (2016)","DOI":"10.1145\/2908080.2908093"},{"key":"39_CR29","unstructured":"Raghothaman, M., Reynolds, A., Udupa, A.: The SyGuS Language Standard Version 2.0, p. 22 (2019)"},{"key":"39_CR30","doi-asserted-by":"crossref","unstructured":"Ramsay, S.J., Neatherway, R.P., Ong, C.H.L.: A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of the 41st ACM Symposium on Principles of Programming Languages, POPL 2014 (2014)","DOI":"10.1145\/2535838.2535873"},{"key":"39_CR31","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. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"key":"39_CR32","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. In: Proceedings of the 28th ACM Conference on Programming Language Design and Implementation, PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250754"},{"key":"39_CR33","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: Proceedings of the 29th ACM Conference on Programming Language Design and Implementation, PLDI 2008 (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"39_CR34","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 404\u2013415, ASPLOS XII (2006)","DOI":"10.1145\/1168857.1168907"},{"issue":"1","key":"39_CR35","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"PD Summers","year":"1977","unstructured":"Summers, P.D.: A methodology for LISP program construction from examples. J. ACM 24(1), 161\u2013175 (1977)","journal-title":"J. ACM"},{"key":"39_CR36","unstructured":"Victor, N.: Synduce. https:\/\/github.com\/victornicolet\/Synduce"},{"key":"39_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-030-30048-7_35","volume-title":"Principles and Practice of Constraint Programming","author":"W Yang","year":"2019","unstructured":"Yang, W., Fedyukovich, G., Gupta, A.: Lemma synthesis for automating induction over algebraic data types. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 600\u2013617. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_35"}],"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_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:12:23Z","timestamp":1626480743000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_39","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)"}}]}}