{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:48:05Z","timestamp":1777765685498,"version":"3.51.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_10","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:15Z","timestamp":1756551855000},"page":"207-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["$$CTL^*$$ Verification and\u00a0Synthesis Using Existential Horn Clauses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-2181-8205","authenticated-orcid":false,"given":"Mishel","family":"Carelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9682-3312","authenticated-orcid":false,"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Brockschmidt, M., Rybalchenko, A.: CTL+FO verification as constraint solving (2014)","DOI":"10.1145\/2632362.2632364"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 221\u2013234. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535860","DOI":"10.1145\/2535838.2535860"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Efficient CTL verification via horn constraints solving. In: Gallagher, J.P., R\u00fcmmer, P. (eds.) Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016. EPTCS, vol.\u00a0219, pp. 1\u201314 (2016). https:\/\/doi.org\/10.4204\/EPTCS.219.1","DOI":"10.4204\/EPTCS.219.1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification, pp. 24\u201351. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Static Analysis","author":"N Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105\u2013125. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LTL synthesis. Electron. Proc. Theor. Comput. Sci. 260, 4\u201322 (2017). https:\/\/doi.org\/10.4204\/eptcs.260.4","DOI":"10.4204\/eptcs.260.4"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Carelli, M., Grumberg, O.: $${CTL}^*$$ verification and synthesis using existential horn clauses. In: 22nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2024, Kyoto, Japan. Springer (2024)","DOI":"10.1007\/978-3-031-78750-8_9"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-319-21690-4_2","volume-title":"Computer Aided Verification","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 13\u201329. Springer, Cham (2015)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Dam, M.: CTL$$^*$$ and ECTL$$^*$$ as fragments of the modal $$\\mu $$-calculus. Theor. Comput. Sci. 126(1), 77\u201396 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90269-0, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397594902690","DOI":"10.1016\/0304-3975(94)90269-0"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Synthesis of reactive systems, pp. 72\u201398 (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends\u00ae Program. Lang. 4(1-2), 1\u2013119 (2017). https:\/\/doi.org\/10.1561\/2500000010","DOI":"10.1561\/2500000010"},{"key":"10_CR14","unstructured":"Guo, D., Svyatkovskiy, A., Yin, J., Duan, N., Brockschmidt, M., Allamanis, M.: Learning to complete code with sketches (2022)"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","volume":"331","author":"Y Kesten","year":"2005","unstructured":"Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comput. Sci. 331, 397\u2013428 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2004.09.023","journal-title":"Theor. Comput. Sci."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-63390-9_18","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2017","unstructured":"Khalimov, A., Bloem, R.: Bounded synthesis for Streett, Rabin, and $$\\text{CTL}^{*}$$. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part II. LNCS, vol. 10427, pp. 333\u2013352. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_18"},{"issue":"2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000). https:\/\/doi.org\/10.1145\/333979.333987","journal-title":"J. ACM"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Long, F., Rinard, M.: Staged program repair with condition synthesis, pp. 166\u2013178 (2015). https:\/\/doi.org\/10.1145\/2786805.2786811","DOI":"10.1145\/2786805.2786811"},{"issue":"1\u20132","key":"10_CR19","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","volume":"163","author":"D Niwi\u0144ski","year":"1996","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: Games for the $$\\mu $$-calculus. Theoret. Comput. Sci. 163(1\u20132), 99\u2013116 (1996)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: 2004 Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32\u201341 (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319598","DOI":"10.1109\/LICS.2004.1319598"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-031-33170-1_23","volume-title":"NASA Formal Methods","author":"BC Rothenberg","year":"2023","unstructured":"Rothenberg, B.C., Grumberg, O., Vizel, Y., Singher, E.: Condition synthesis realizability via constrained horn clauses. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods, pp. 380\u2013396. Springer, Cham (2023)"},{"issue":"5","key":"10_CR22","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/1168919.1168907","volume":"34","author":"A Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. SIGARCH Comput. Archit. News 34(5), 404\u2013415 (2006). https:\/\/doi.org\/10.1145\/1168919.1168907","journal-title":"SIGARCH Comput. Archit. News"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. Int. J. Softw. Tools Technol. Transf. 15(5), 497\u2013518 (2012). https:\/\/www.microsoft.com\/en-us\/research\/publication\/template-based-program-verification-program-synthesis\/","DOI":"10.1007\/s10009-012-0223-4"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571265","DOI":"10.1145\/3571265"},{"key":"10_CR25","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. (eds.) Computer Aided Verification, pp. 742\u2013766. Springer, Cham (2021)"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Xiong, Y., Wang, J., Yan, R., Zhang, J., Han, S., Huang, G., Zhang, L.: Precise condition synthesis for program repair. In: 2017 IEEE\/ACM 39th International Conference on Software Engineering (ICSE), pp. 416\u2013426 (2017). https:\/\/doi.org\/10.1109\/ICSE.2017.45","DOI":"10.1109\/ICSE.2017.45"},{"issue":"1","key":"10_CR27","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/TSE.2016.2560811","volume":"43","author":"J Xuan","year":"2017","unstructured":"Xuan, J., et al.: Nopol: automatic repair of conditional statement bugs in java programs. IEEE Trans. Softw. Eng. 43(1), 34\u201355 (2017). https:\/\/doi.org\/10.1109\/TSE.2016.2560811","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:28:07Z","timestamp":1777476487000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}