{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:39:06Z","timestamp":1743068346163,"version":"3.40.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present a new synthesis method based on the novel concept of a <jats:italic>constraint annotated tree automaton (CATA)<\/jats:italic>. A CATA is a variant of a finite tree automaton (FTA) where the acceptance of a term by the automaton is conditioned upon the logical satisfiability of a formula. In the context of program synthesis, CATAs allow the construction of a more precise version space than FTAs by ruling out programs that make inconsistent assumptions about the unknown semantics of functions under synthesis. We apply our proposed algorithm to synthesizing recursive (or mutually recursive) procedures from relational specifications and demonstrate that our method allows solving synthesis problems that are beyond the scope of existing approaches.\n<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_3","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"41-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Relational Synthesis of\u00a0Recursive Programs via\u00a0Constraint Annotated Tree Automata"],"prefix":"10.1007","author":[{"given":"Anders","family":"Miltner","sequence":"first","affiliation":[]},{"given":"Ziteng","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Swarat","family":"Chaudhuri","sequence":"additional","affiliation":[]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"3_CR1","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":"3_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"6","key":"3_CR3","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/3140587.3062378","volume":"52","author":"T Antonopoulos","year":"2017","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. ACM SIGPLAN Notices 52(6), 362\u2013375 (2017)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Barnaby, C., Chen, Q., Samanta, R., Dillig, I.: Imageeye: batch image processing using program synthesis. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591248","DOI":"10.1145\/3591248"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/982962.964003","volume":"39","author":"N Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Not. 39(1), 14\u201325 (2004)","journal-title":"ACM SIGPLAN Not."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"862","DOI":"10.1007\/978-3-540-73420-8_74","volume-title":"Automata, Languages and Programming","author":"H Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Boja\u0144czyk, M.: Bounded depth data trees. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 862\u2013874. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73420-8_74"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Chen, J., Wei, J., Feng, Y., Bastani, O., Dillig, I.: Relational verification using reinforcement learning. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201330 (2019)","DOI":"10.1145\/3360567"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Q., Wang, X., Ye, X., Durrett, G., Dillig, I.: Multi-modal synthesis of regular expressions. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 487\u2013502 (2020)","DOI":"10.1145\/3385412.3385988"},{"issue":"OOPSLA2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/3563308","volume":"6","author":"Y Chen","year":"2022","unstructured":"Chen, Y., Wang, Y., Goyal, M., Dong, J., Feng, Y., Dillig, I.: Synthesis-powered optimization of smart contracts via data type refactoring. Proc. ACM Program. Lang. 6(OOPSLA2), 560\u2013588 (2022)","journal-title":"Proc. ACM Program. Lang."},{"issue":"9","key":"3_CR11","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"K Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of haskell programs. SIGPLAN Not. 35(9), 268\u2013279 (2000). https:\/\/doi.org\/10.1145\/357766.351266","journal-title":"SIGPLAN Not."},{"key":"3_CR12","unstructured":"Comon, H., et al.: Tree automata techniques and applications (2008)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-79124-9_12","volume-title":"Tests and Proofs","author":"J de Halleux","year":"2008","unstructured":"de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 171\u2013181. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_12"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Farzan, A., Lette, D., Nicolet, V.: Recursion synthesis with unrealizability witnesses. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2022, New York, NY, USA, pp. 244\u2013259. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3519939.3523726","DOI":"10.1145\/3519939.3523726"},{"issue":"4","key":"3_CR15","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1145\/3296979.3192382","volume":"53","author":"Y Feng","year":"2018","unstructured":"Feng, Y., Martins, R., Bastani, O., Dillig, I.: Program synthesis using conflict-driven learning. SIGPLAN Not. 53(4), 420\u2013435 (2018). https:\/\/doi.org\/10.1145\/3296979.3192382","journal-title":"SIGPLAN Not."},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Feng, Y., Martins, R., Van\u00a0Geffen, J., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017, New York, NY, USA, pp. 422\u2013436. Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3062341.3062351","DOI":"10.1145\/3062341.3062351"},{"issue":"6","key":"3_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/2813885.2737977","volume":"50","author":"JK Feser","year":"2015","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. SIGPLAN Not. 50(6), 229\u2013239 (2015). https:\/\/doi.org\/10.1145\/2813885.2737977","journal-title":"SIGPLAN Not."},{"issue":"4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/263244.263267","volume":"22","author":"G Fink","year":"1997","unstructured":"Fink, G., Bishop, M.: Property-based testing: a new approach to testing for assurance. ACM SIGSOFT Software Eng. Not. 22(4), 74\u201380 (1997)","journal-title":"ACM SIGSOFT Software Eng. Not."},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1145\/2914770.2837629","volume":"51","author":"J Frankle","year":"2016","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. SIGPLAN Not. 51(1), 802\u2013815 (2016). https:\/\/doi.org\/10.1145\/2914770.2837629","journal-title":"SIGPLAN Not."},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201911, New York, NY, USA, pp. 317\u2013330. Association for Computing Machinery (2011). https:\/\/doi.org\/10.1145\/1926385.1926423","DOI":"10.1145\/1926385.1926423"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Guo, Z., Cao, D., Tjong, D., Yang, J., Schlesinger, C., Polikarpova, N.: Type-directed program synthesis for restful apis. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2022, New York, NY, USA, pp. 122\u2013136. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3519939.3523450","DOI":"10.1145\/3519939.3523450"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Hu, Q., D\u2019Antoni, L.: Automatic program inversion using symbolic transducers. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 376\u2013389 (2017)","DOI":"10.1145\/3062341.3062345"},{"key":"3_CR23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316784099","volume-title":"Programming in Haskell","author":"G Hutton","year":"2016","unstructured":"Hutton, G.: Programming in Haskell, 2nd edn. Cambridge University Press, Cambridge (2016)","edition":"2"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, R.N.S., Sergey, I.: Cyclic program synthesis. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021, New York, NY, USA, pp. 944\u2013959. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454087","DOI":"10.1145\/3453483.3454087"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Tan, T.: Tree automata over infinite alphabets. In: Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pp. 386\u2013423 (2008)","DOI":"10.1007\/978-3-540-78127-1_21"},{"key":"3_CR26","unstructured":"Kitzelmann, E., Schmid, U., Olsson, R., Kaelbling, L.P.: Inductive synthesis of functional programs: an explanation based generalization approach. J. Mach. Learn. Res. 7(2) (2006)"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications. OOPSLA \u201913, New York, NY, USA, pp. 407\u2013426. Association for Computing Machinery (2013). https:\/\/doi.org\/10.1145\/2509136.2509555, https:\/\/doi.org\/10.1145\/2509136.2509555","DOI":"10.1145\/2509136.2509555 10.1145\/2509136.2509555"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Lampropoulos, L., Hicks, M., Pierce, B.C.: Coverage guided, property based testing. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201329 (2019)","DOI":"10.1145\/3360607"},{"key":"3_CR29","unstructured":"Lampropoulos, L., Pierce, B.C.: QuickChick: Property-Based Testing in Coq. Software Foundations series, volume 4, Electronic textbook (2018)"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Lee, W., Cho, H.: Inductive synthesis of structurally recursive functional programs from non-recursive expressions. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571263","DOI":"10.1145\/3571263"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Lubin, J., Collins, N., Omar, C., Chugh, R.: Program sketching with live bidirectional evaluation. Proc. ACM Program. Lang. 4(ICFP) (2020). https:\/\/doi.org\/10.1145\/3408991","DOI":"10.1145\/3408991"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Mariano, B., Chen, Y., Feng, Y., Durrett, G., Dillig, I.: Automated transpilation of imperative to functional code using neural-guided program synthesis. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527315","DOI":"10.1145\/3527315"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Miltner, A., Nu\u00f1ez, A.T., Brendel, A., Chaudhuri, S., Dillig, I.: Bottom-up synthesis of recursive functional programs using angelic execution. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498682","DOI":"10.1145\/3498682"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Miltner, A., Padhi, S., Millstein, T., Walker, D.: Data-driven inference of representation invariants. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2020, New York, NY, USA, pp. 1\u201315. Association for Computing Machinery (2020). https:\/\/doi.org\/10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI \u201915, New York, NY, USA, pp. 619\u2013630. Association for Computing Machinery (2015). https:\/\/doi.org\/10.1145\/2737924.2738007","DOI":"10.1145\/2737924.2738007"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Pailoor, S., Wang, Y., Dillig, I.: Semantic code refactoring for abstract data types. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632870","DOI":"10.1145\/3632870"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Pailoor, S., Wang, Y., Wang, X., Dillig, I.: Synthesizing data structure refinements from integrity constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021, New York, NY, USA, pp. 574\u2013587. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454063","DOI":"10.1145\/3453483.3454063"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-96145-3_9","volume-title":"Computer Aided Verification","author":"L Pick","year":"2018","unstructured":"Pick, L., Fedyukovich, G., Gupta, A.: Exploiting synchrony and symmetry in relational verification. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 164\u2013182. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_9"},{"key":"3_CR39","doi-asserted-by":"publisher","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. PLDI \u201916, New York, NY, USA, pp. 522\u2013538. Association for Computing Machinery (2016). https:\/\/doi.org\/10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Samak, M., Kim, D., Rinard, M.C.: Synthesizing replacement classes. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371120","DOI":"10.1145\/3371120"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404\u2013415. ACM (2006). https:\/\/doi.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"issue":"6","key":"3_CR42","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/2980983.2908092","volume":"51","author":"M Sousa","year":"2016","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. SIGPLAN Not. 51(6), 57\u201369 (2016). https:\/\/doi.org\/10.1145\/2980983.2908092","journal-title":"SIGPLAN Not."},{"issue":"1","key":"3_CR43","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). https:\/\/doi.org\/10.1145\/321992.322002","journal-title":"J. ACM"},{"issue":"5","key":"3_CR44","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/1095430.1081749","volume":"30","author":"N Tillmann","year":"2005","unstructured":"Tillmann, N., Schulte, W.: Parameterized unit tests. ACM SIGSOFT Software Eng. Not. 30(5), 253\u2013262 (2005)","journal-title":"ACM SIGSOFT Software Eng. Not."},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1007\/978-3-030-81685-8_35","volume-title":"Computer Aided Verification","author":"H Unno","year":"2021","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational verification. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 742\u2013766. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35"},{"issue":"3","key":"3_CR46","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1016\/j.ipl.2014.11.005","volume":"115","author":"M Veanes","year":"2015","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic tree automata. Inf. Process. Lett. 115(3), 418\u2013424 (2015)","journal-title":"Inf. Process. Lett."},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Wang, C., Cheung, A., Bodik, R.: Interactive query synthesis from input-output examples. In: Proceedings of the 2017 ACM International Conference on Management of Data, pp. 1631\u20131634. SIGMOD \u201917, Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3035918.3058738, https:\/\/doi.org\/10.1145\/3035918.3058738","DOI":"10.1145\/3035918.3058738 10.1145\/3035918.3058738"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Wang, C., Feng, Y., Bodik, R., Dillig, I., Cheung, A., Ko, A.J.: Falx: synthesis-powered visualization authoring. In: Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems. CHI \u201921, New York, NY, USA. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3411764.3445249","DOI":"10.1145\/3411764.3445249"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158151","DOI":"10.1145\/3158151"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Wang, X., Dillig, I., Singh, R.: Synthesis of data completion scripts using finite tree automata. Proc. ACM Program. Lang. 1(OOPSLA) (2017). https:\/\/doi.org\/10.1145\/3133886","DOI":"10.1145\/3133886"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Wang, Y., Wang, X., Dillig, I.: Relational program synthesis. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276525","DOI":"10.1145\/3276525"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Yaghmazadeh, N., Wang, Y., Dillig, I., Dillig, T.: Sqlizer: query synthesis from natural language. Proc. ACM Program. Lang. 1(OOPSLA), 1\u201326 (2017)","DOI":"10.1145\/3133887"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Yuan, Y., Radhakrishna, A., Samanta, R.: Trace-guided inductive synthesis of recursive functional programs. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591255","DOI":"10.1145\/3591255"}],"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-031-65633-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:27Z","timestamp":1721891007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}