{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:08Z","timestamp":1740122768097,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T00:00:00Z","timestamp":1684195200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T00:00:00Z","timestamp":1684195200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["Discovery"],"award-info":[{"award-number":["Discovery"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,10]]},"DOI":"10.1007\/s10703-023-00417-y","type":"journal-article","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T09:02:24Z","timestamp":1684227744000},"page":"172-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Partial bounding for recursive function synthesis"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[]},{"given":"Victor","family":"Nicolet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,16]]},"reference":[{"key":"417_CR1","doi-asserted-by":"crossref","unstructured":"Abrahamsson O, Myreen MO (2018) Automatically introducing tail recursion in CakeML. In: Trends in functional programming, lecture notes in computer science. Springer International Publishing, pp 118\u2013134","DOI":"10.1007\/978-3-319-89719-6_7"},{"key":"417_CR2","doi-asserted-by":"crossref","unstructured":"Ahmad MBS, Cheung A (2018) Automatically leveraging mapreduce frameworks for data-intensive applications. In: Proceedings of the 2018 international conference on management of data, SIGMOD \u201918. ACM","DOI":"10.1145\/3183713.3196891"},{"key":"417_CR3","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: Computer aided verification, lecture notes in computer science. Springer, pp 934\u2013950","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"417_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Bodik R, Juniwal G, et\u00a0al (2013) Syntax-guided synthesis. In: 2013 Formal methods in computer-aided design. IEEE, pp 1\u20138","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"417_CR5","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway CL, Deters M et al (2011) CVC4. Computer aided verification. In: Lecture notes in computer science. Springer, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"417_CR6","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall RM, Darlington J (1977) A transformation system for developing recursive programs. J ACM 24(1):44\u201367","journal-title":"J ACM"},{"key":"417_CR7","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"417_CR8","doi-asserted-by":"crossref","unstructured":"Farzan A, Nicolet V (2017) Synthesis of divide and conquer parallelism for loops. In: Proceedings of the 38th ACM conference on programming language design and implementation, PLDI \u201917","DOI":"10.1145\/3062341.3062355"},{"key":"417_CR9","doi-asserted-by":"crossref","unstructured":"Fedyukovich G, Ahmad MBS, Bodik R (2017) 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","DOI":"10.1145\/3062341.3062382"},{"key":"417_CR10","doi-asserted-by":"crossref","unstructured":"Feldman YMY, Padon O, Immerman N, et\u00a0al (2017) Bounded quantifier instantiation for checking inductive invariants. In: Tools and algorithms for the construction and analysis of systems, lecture notes in computer science, pp 76\u201395","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"417_CR11","doi-asserted-by":"crossref","unstructured":"Feser JK, Chaudhuri S, Dillig I (2015) Synthesizing data structure transformations from input\u2013output examples. In: Proceedings of the 36th ACM conference on programming language design and implementation, PLDI \u201915","DOI":"10.1145\/2737924.2737977"},{"key":"417_CR12","doi-asserted-by":"crossref","unstructured":"Frankle J, Osera PM, Walker D, et\u00a0al (2016) Example-directed synthesis: a type-theoretic interpretation. In: Proceedings of the 43rd ACM symposium on principles of programming languages, POPL\u201916","DOI":"10.1145\/2837614.2837629"},{"key":"417_CR13","doi-asserted-by":"crossref","unstructured":"Hamilton GW, Jones ND (2012) Distillation with labelled transition systems. In: Proceedings of the ACM 2012 workshop on partial evaluation and program manipulation, PEPM \u201912. ACM, pp 15\u201324","DOI":"10.1145\/2103746.2103753"},{"key":"417_CR14","doi-asserted-by":"crossref","unstructured":"Huet G (1997) The zipper. J Funct Program 7(5)","DOI":"10.1017\/S0956796897002864"},{"key":"417_CR15","doi-asserted-by":"crossref","unstructured":"Inala JP, Polikarpova N, Qiu X, et\u00a0al (2017) Synthesis of recursive ADT transformations from reusable templates. In: Tools and algorithms for the construction and analysis of systems, lecture notes in computer science","DOI":"10.1007\/978-3-662-54577-5_14"},{"key":"417_CR16","doi-asserted-by":"crossref","unstructured":"Itzhaky S, Singh R, Solar-Lezama A, et\u00a0al (2016) 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. ACM, pp 145\u2013164","DOI":"10.1145\/2983990.2983993"},{"key":"417_CR17","doi-asserted-by":"crossref","unstructured":"Katayama S (2012) An analytical inductive functional programming system that avoids unintended programs. In: Proceedings of the 2012 workshop on partial evaluation and program manipulation, PEPM\u201912","DOI":"10.1145\/2103746.2103758"},{"issue":"15","key":"417_CR18","first-page":"429","volume":"7","author":"E Kitzelmann","year":"2006","unstructured":"Kitzelmann E, Schmid U (2006) Inductive synthesis of functional programs: an explanation based generalization approach. J Mach Learn Res 7(15):429\u2013454","journal-title":"J Mach Learn Res"},{"key":"417_CR19","doi-asserted-by":"crossref","unstructured":"Kneuss E, Kuraj I, Kuncak V, et\u00a0al (2013) Synthesis modulo recursive functions. In: Proceedings of the 2013 international conference on object oriented programming systems languages and applications, OOPSLA\u201913","DOI":"10.1145\/2509136.2509555"},{"key":"417_CR20","doi-asserted-by":"crossref","unstructured":"Kobayashi N (2009) 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\u201909","DOI":"10.1145\/1480881.1480933"},{"key":"417_CR21","doi-asserted-by":"crossref","unstructured":"Kobayashi N, Tabuchi N, Unno H (2010) 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\u201910","DOI":"10.1145\/1706299.1706355"},{"key":"417_CR22","doi-asserted-by":"crossref","unstructured":"Kobayashi N, Sato R, Unno H (2011) Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM conference on programming language design and implementation, PLDI\u201911, pp 222\u2013233","DOI":"10.1145\/1993498.1993525"},{"key":"417_CR23","unstructured":"Leroy X, Doligez D, Frisch A, et\u00a0al (2019) The OCaml system release 4.11: documentation and user\u2019s manual. p 823"},{"key":"417_CR24","doi-asserted-by":"crossref","unstructured":"Morihata A, Matsuzaki K (2010) Automatic parallelization of recursive functions using quantifier elimination. In: Proceedings of the 10th international conference on functional and logic programming, FLOPS\u201910","DOI":"10.1007\/978-3-642-12251-4_23"},{"key":"417_CR25","doi-asserted-by":"crossref","unstructured":"Morihata A, Matsuzaki K, Hu Z, et\u00a0al (2009) The third homomorphism theorem on trees: downward and upward lead to divide-and-conquer. In: Proceedings of the 36th ACM symposium on principles of programming languages, POPL\u201909","DOI":"10.1145\/1480881.1480905"},{"key":"417_CR26","unstructured":"Nicolet V (2022) Synduce. https:\/\/github.com\/synduce\/Synduce\/releases\/tag\/fmsd22"},{"key":"417_CR27","doi-asserted-by":"crossref","unstructured":"Ong CHL, Ramsay SJ (2011) Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of the 38th ACM symposium on principles of programming languages, POPL\u201911","DOI":"10.1145\/1926385.1926453"},{"key":"417_CR28","doi-asserted-by":"crossref","unstructured":"Osera PM, Zdancewic S (2015) Type-and-example-directed program synthesis. In: Proceedings of the 36th ACM conference on programming language design and implementation, PLDI\u201915","DOI":"10.1145\/2737924.2738007"},{"key":"417_CR29","unstructured":"Padhi S, Polgreen E, Raghothaman M, et\u00a0al (2019) The SyGuS language standard version 2.1"},{"key":"417_CR30","doi-asserted-by":"crossref","unstructured":"Polikarpova N, Kuraj I, Solar-Lezama A (2016) Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM conference on programming language design and implementation, PLDI\u201916","DOI":"10.1145\/2908080.2908093"},{"key":"417_CR31","doi-asserted-by":"crossref","unstructured":"Ramsay SJ, Neatherway RP, Ong CHL (2014) A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of the 41st ACM symposium on principles of programming languages, POPL\u201914","DOI":"10.1145\/2535838.2535873"},{"key":"417_CR32","doi-asserted-by":"crossref","unstructured":"Reynolds A, Deters M, Kuncak V, et\u00a0al (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification, lecture notes in computer science, pp 198\u2013216","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"417_CR33","volume-title":"Program synthesis by sketching","author":"A Solar-Lezama","year":"2008","unstructured":"Solar-Lezama A (2008) Program synthesis by sketching. University of California, Berkeley"},{"key":"417_CR34","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Tancau L, Bodik R, et\u00a0al (2006) Combinatorial sketching for finite programs. In: Proceedings of the 12th international conference on architectural support for programming languages and operating systems, ASPLOS XII. pp 404\u2013415","DOI":"10.1145\/1168857.1168907"},{"key":"417_CR35","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Arnold G, Tancau L, et\u00a0al (2007) Sketching stencils. In: Proceedings of the 28th ACM conference on programming language design and implementation, PLDI\u201907","DOI":"10.1145\/1250734.1250754"},{"key":"417_CR36","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Jones CG, Bodik R (2008) Sketching concurrent data structures. In: Proceedings of the 29th ACM conference on programming language design and implementation, PLDI\u201908","DOI":"10.1145\/1375581.1375599"},{"issue":"1","key":"417_CR37","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"PD Summers","year":"1977","unstructured":"Summers PD (1977) A methodology for LISP program construction from examples. J ACM 24(1):161\u2013175","journal-title":"J ACM"},{"key":"417_CR38","doi-asserted-by":"crossref","unstructured":"Yang W, Fedyukovich G, Gupta A (2019) Lemma synthesis for automating induction over algebraic data types. In: Principles and practice of constraint programming, lecture notes in computer science, pp 600\u2013617","DOI":"10.1007\/978-3-030-30048-7_35"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00417-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00417-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00417-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T17:12:54Z","timestamp":1729530774000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00417-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,16]]},"references-count":38,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["417"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00417-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2023,5,16]]},"assertion":[{"value":"4 February 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}