{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:15Z","timestamp":1784793795745,"version":"3.55.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Component-based synthesis (CBS) aims to generate loop-free programs from a set of libraries whose methods are annotated\u00a0with specifications and whose output must satisfy a set of logical constraints, expressed as a query. The effectiveness of a\u00a0CBS algorithm critically depends on the severity of the constraints imposed by the query. The more exact these constraints are,\u00a0the sparser the space of feasible solutions. This maxim also applies\u00a0when we enrich the expressivity of the specifications affixed to library methods. In both cases, search must now contend with constraints\u00a0that may only hold over a small number of the possible execution paths\u00a0that can be enumerated by a CBS procedure.<\/jats:p>\n                  <jats:p>\n                    In this paper, we address\u00a0this challenge by equipping CBS search with the ability to reason\u00a0about\n                    <jats:italic>logical similarities<\/jats:italic>\n                    among the paths it explores. Our setting considers library methods equipped with refinement-type specifications that enrich ordinary base types with a set of rich logical qualifiers to constrain the set of values accepted by that type.\n                  <\/jats:p>\n                  <jats:p>\n                    For efficient representation and enumeration of this space,\u00a0we introduce a novel tree automata variant called\n                    <jats:italic>Liquid Tree Automata<\/jats:italic>\n                    \u00a0 (LTA)\u00a0whose construction is driven by the typing rules of a refinement\u00a0type system. This allows us to leverage subtyping constraints over\u00a0the refinement types associated with enumerated terms to enable reasoning about similarity among candidate solutions as search proceeds,\u00a0using this notion of similarity to eagerly merge LTA states. By doing so, we avoid exploration of semantically similar paths, leading to\u00a0a significantly improved search procedure. We present an implementation of this idea in a tool called \u00a0 and provide a comprehensive evaluation that demonstrates \u2019s ability to synthesize solutions to complex CBS queries that go well-beyond the capabilities of\u00a0the existing state-of-the-art.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_15","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:14Z","timestamp":1784791094000},"page":"284-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Liquid Tree Automata"],"prefix":"10.1007","author":[{"given":"Ashish","family":"Mishra","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"15_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"},{"issue":"POPL","key":"15_CR2","doi-asserted-by":"publisher","first-page":"1182","DOI":"10.1145\/3571234","volume":"7","author":"M Bowers","year":"2023","unstructured":"Bowers, M., et al.: Top-down synthesis for library learning. Proc. ACM Program. Lang. 7(POPL), 1182\u20131213 (2023)","journal-title":"Proc. ACM Program. Lang."},{"issue":"POPL","key":"15_CR3","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/3571207","volume":"7","author":"D Cao","year":"2023","unstructured":"Cao, D., Kunkel, R., Nandi, C., Willsey, M., Tatlock, Z., Polikarpova, N.: babble: Learning better abstractions with e-graphs and anti-unification. Proc. ACM Program. Lang. 7(POPL), 396\u2013424 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR4","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.C., Pereira, M., Pottier, F.: VOCAL \u2013 a verified OCaml library. In: ML Family Workshop (2017)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Comon, H.: Tree Automata Techniques and Applications (1997)","DOI":"10.1007\/3-540-62950-5"},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10703-015-0233-4","volume":"47","author":"L D\u2019antoni","year":"2015","unstructured":"D\u2019antoni, L., Veanes, M.: Extended symbolic finite automata and transducers. Form. Methods Syst. Des. 47(1), 93\u2013119 (2015)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1006\/jsco.1995.1048","volume":"20","author":"M Dauchet","year":"1995","unstructured":"Dauchet, M., Caron, A.-C., Coquid\u00e9, J.-L.: Automata for reduction properties solving. J. Symb. Comput. 20(2), 215\u2013233 (1995)","journal-title":"J. Symb. Comput."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Bastani, O., Dillig, I.: Program synthesis using conflict-driven learning. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 420\u2013435. Association for Computing Machinery, New York (2018)","DOI":"10.1145\/3192366.3192382"},{"key":"15_CR9","doi-asserted-by":"crossref","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, pp. 422\u2013436. Association for Computing Machinery, New York (2017)","DOI":"10.1145\/3062341.3062351"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 599\u2013612. Association for Computing Machinery, New York (2017)","DOI":"10.1145\/3009837.3009851"},{"issue":"OOPSLA2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"912","DOI":"10.1145\/3622830","volume":"7","author":"J Feser","year":"2023","unstructured":"Feser, J., Dillig, I., Solar-Lezama, A.: Inductive program synthesis guided by observational program similarity. Proc. ACM Program. Lang. 7(OOPSLA2), 912\u2013940 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Synthesizing functional reactive programs. In: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell 2019, pp. 162\u2013175. Association for Computing Machinery, New York (2019)","DOI":"10.1145\/3331545.3342601"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI \u201993, pp. 237\u2013247. Association for Computing Machinery, New York (1993)","DOI":"10.1145\/155090.155113"},{"issue":"POPL","key":"15_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3371080","volume":"4","author":"Z Guo","year":"2019","unstructured":"Guo, Z., et al.: Program synthesis by type-guided abstraction refinement. Proc. ACM Program. Lang. 4(POPL), 1\u201328 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Guria, S.N., Foster, J.S., Van\u00a0Horn, D.: RbSyn: type- and effect-guided program synthesis. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 344\u2013358. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3453483.3454048"},{"key":"15_CR16","unstructured":"Itzhaky, S., et al.: On the automated verification of web applications with embedded SQL. In: Benedikt, M., Orsi, G. (eds.) 20th International Conference on Database Theory, ICDT 2017, Venice, Italy, 21\u201324 March 2017, vol.\u00a068 of LIPIcs, pp. 16:1\u201316:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"issue":"OOPSLA","key":"15_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428273","volume":"4","author":"MB James","year":"2020","unstructured":"James, M.B., et al.: Digging for fold: synthesis-aided API discovery for haskell. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201327 (2020)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, vol. 1, ICSE \u201910, pp. 215\u2013224. Association for Computing Machinery, New York (2010)","DOI":"10.1145\/1806799.1806833"},{"issue":"3\u20134","key":"15_CR19","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1561\/2500000032","volume":"6","author":"R Jhala","year":"2021","unstructured":"Jhala, R., Vazou, N.: Refinement types: a tutorial. Found. Trends Program. Lang. 6(3\u20134), 159\u2013317 (2021)","journal-title":"Found. Trends Program. Lang."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Kaki, G., Jagannathan, S.: A relational framework for higher-order shape analysis. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP \u201914, pp. 311\u2013324. Association for Computing Machinery, New York (2014)","DOI":"10.1145\/2628136.2628159"},{"issue":"ICFP","key":"15_CR21","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/3547622","volume":"6","author":"J Koppel","year":"2022","unstructured":"Koppel, J., Guo, Z., de Vries, E., Solar-Lezama, A., Polikarpova, N.: Searching entangled program spaces. Proc. ACM Program. Lang. 6(ICFP), 23\u201351 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR22","unstructured":"Lau, T.A., Domingos, P., Weld, D.S.: Version space algebra and its application to programming by demonstration. In: Proceedings of the Seventeenth International Conference on Machine Learning, ICML \u201900, pp. 527\u2013534. Morgan Kaufmann Publishers Inc., San Francisco (2000)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498682","volume":"6","author":"A Miltner","year":"2022","unstructured":"Miltner, A., Nu\u00f1ez, A.T., Brendel, A., Chaudhuri, S., Dilig, I.: Bottom-up synthesis of recursive functional programs using angelic execution. Proc. ACM Program. Lang. 6, 1\u201329 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Miltner, A., Wang, Z., Chaudhuri, S., Dillig, I.: Relational synthesis of recursive programs via constraint annotated tree automata. In: Computer Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, 24\u201327 July 2024, Proceedings, Part III, pp. 41\u201363. Springer-Verlag, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_3","DOI":"10.1007\/978-3-031-65633-0_3"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Mishra, A., Jaganathan, S.: Artifact for the CAV 2026 Paper: Liquid Tree Automata. Zenodo (2026). https:\/\/doi.org\/10.5281\/zenodo.19821156","DOI":"10.5281\/zenodo.19821156"},{"issue":"OOPSLA2","key":"15_CR26","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1145\/3563310","volume":"6","author":"A Mishra","year":"2022","unstructured":"Mishra, A., Jagannathan, S.: Specification-guided component-based synthesis from effectful libraries. Proc. ACM Program. Lang. 6(OOPSLA2), 616\u2013645 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR27","unstructured":"Mishra, A., Jagannathan, S.: Liquid Tree Automata (2026). https:\/\/arxiv.org\/abs\/2605.13456"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Abstract Interpretation, pp. 211\u2013282. Springer, Heidelberg (1999)","DOI":"10.1007\/978-3-662-03811-6_4"},{"key":"15_CR29","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, PLDI \u201916, pp. 522\u2013538. Association for Computing Machinery, New York (2016)","DOI":"10.1145\/2908080.2908093"},{"issue":"POPL","key":"15_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290386","volume":"3","author":"K Shi","year":"2019","unstructured":"Shi, K., Steinhardt, J., Liang, P.: FrAngel: component-based synthesis with control structures. Proc. ACM Program. Lang. 3(POPL), 1\u201329 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-030-11245-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Smith","year":"2019","unstructured":"Smith, C., Albarghouthi, A.: Program synthesis with equivalence reduction. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 24\u201347. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_2"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pp. 387\u2013398. Association for Computing Machinery, New York (2013)","DOI":"10.1145\/2491956.2491978"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Vazou, N., Bakst, A., Jhala, R.: Bounded refinement types. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 48\u201361. Association for Computing Machinery, New York (2015)","DOI":"10.1145\/2784731.2784745"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37036-6_13","volume-title":"Programming Languages and Systems","author":"N Vazou","year":"2013","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209\u2013228. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Wang, C., Feng, Y., Bodik, R., Cheung, A.,Dillig, I : Visualization by example. Proc. ACM Program. Lang. 4(POPL) (2019)","DOI":"10.1145\/3371117"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. Proc. ACM Program. Lang. 2(POPL) (2017)","DOI":"10.1145\/3158151"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Wang, X., Dillig, I., Singh, R.: Synthesis of data completion scripts using finite tree automata. Proc. ACM Program. Lang. 1(OOPSLA) (2017)","DOI":"10.1145\/3133886"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: Egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL) (2021)","DOI":"10.1145\/3434304"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Zhang, Y., et al.: Better together: unifying datalog and equality saturation. Proc. ACM Program. Lang. 7(PLDI) (2023)","DOI":"10.1145\/3591239"}],"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-032-32519-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:20Z","timestamp":1784791100000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"The\n                      Hegel\n                      tool and the artifact used in the paper is available in [\n                      \n                      ].","order":2,"name":"Ethics","label":"Data Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}