{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:17Z","timestamp":1779074477102,"version":"3.51.4"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    is a recently-proposed SAT-based liveness model checking algorithm that showed remarkable performance compared to other state-of-the-art approaches, both in absolute terms (solving more problems overall than other engines on standard benchmark sets) as well as in relative terms (solving several problems that none of the other engines could solve).  proves or disproves properties of the form\n                    <jats:italic>FGq<\/jats:italic>\n                    , by trying to show that\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\lnot q$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u00ac<\/mml:mo>\n                            <mml:mi>q<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    can be visited only a finite number of times via an incremental reduction to a sequence of reachability queries. A key factor in the good performance of  is the extraction of \u201cshoals\u201d from the inductive invariants of the reachability queries to block states that can reach\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\lnot q$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u00ac<\/mml:mo>\n                            <mml:mi>q<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    a bounded number of times.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we generalize  to handle infinite-state systems, using the Verification Modulo Theories paradigm. In contrast to the finite-state case, liveness cannot be simply reduced to finding a bound on the number of occurrences of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\lnot q$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u00ac<\/mml:mo>\n                            <mml:mi>q<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    on paths. We propose therefore a solution leveraging predicate abstraction and termination techniques based on well-founded relations. In particular, we show how we can extract shoals that take into account the well-founded relations. We implemented the technique on top of the open source VMT engine IC3ia and we experimentally demonstrate how the new extension maintains the performance advantages (both absolute and relative) of the original , thus significantly contributing to advancing the state of the art of infinite-state liveness verification.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_11","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:45:52Z","timestamp":1753130752000},"page":"215-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Infinite-State Liveness Checking with\u00a0rlive"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher","family":"Johannsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250\u2013271 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.,\u00a0Artho, C.,\u00a0Schuppan, V.: Liveness checking as safety checking. In: Proceedings of the 7th International Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 66:2 (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-319-08867-9_55","volume-title":"Computer Aided Verification","author":"J Birgmeier","year":"2014","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831\u2013848. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_55"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Bliudze, S., et al.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326\u2013343. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_25","DOI":"10.1007\/978-3-319-24953-7_25"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bombardelli, A., Cimatti, A., Griggio, A., Tonetta, S.: Another look at LTL modulo theory over finite and infinite traces. In: Principles of Verification (1), vol. 15260. LNCS, pp. 419\u2013443. Springer (2024)","DOI":"10.1007\/978-3-031-75783-9_17"},{"key":"11_CR8","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 144\u2013153. IEEE (2011)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413\u2013429. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_28"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Magnago, E.: LTL falsification in infinite-state systems. Inf. Comput. 289(Part), 104977 (2022)","DOI":"10.1016\/j.ic.2022.104977"},{"issue":"3","key":"11_CR11","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/s10703-023-00434-x","volume":"60","author":"A Cimatti","year":"2022","unstructured":"Cimatti, A., Griggio, A., Mover, S., Roveri, M., Tonetta, S.: Verification modulo theories. Formal Methods Syst. Des. 60(3), 452\u2013481 (2022)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-319-08867-9_28","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL properties of hybrid systems with K-Liveness. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 424\u2013440. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_28"},{"issue":"3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-016-0257-4","volume":"49","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst. Des. 49(3), 190\u2013218 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0257-4","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"11_CR15","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: The VMT-LIB language and tools. In: SMT, volume 3185 of CEUR Workshop Proceedings, pp. 80\u201389. CEUR-WS.org (2022)"},{"key":"11_CR16","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 52\u201359. IEEE (2012)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415\u2013427. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_72"},{"issue":"5","key":"11_CR18","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Yuan, L., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. ACM SIGPLAN Not. 42(1), 265\u2013276 (2007)","DOI":"10.1145\/1190215.1190257"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: International Conference on Computer Aided Verification, pp. 13\u201329. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-22110-1_26","volume-title":"Computer Aided Verification","author":"B Cook","year":"2011","unstructured":"Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 333\u2013348. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_26"},{"issue":"6","key":"11_CR22","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/1133255.1134029","volume":"41","author":"B Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. ACM Sigplan Not. 41(6), 415\u2013426 (2006)","journal-title":"ACM Sigplan Not."},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-41528-4_15","volume-title":"Computer Aided Verification","author":"J Daniel","year":"2016","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 271\u2013291. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Doose, D., Brunel, J.: Simple LTL model checking on finite and infinite traces over concrete domains. In: International Conference on Formal Engineering Methods, pp. 375\u2013390. Springer (2024)","DOI":"10.1007\/978-981-96-0617-7_21"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Neural model checking. In: Advances in Neural Information Processing Systems 37 (NeurIPS 2024). NeurIPS (2024)","DOI":"10.52202\/079017-2742"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 633\u2013645 (2022)","DOI":"10.1145\/3540250.3549120"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Graf, S.,\u00a0Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"11_CR29","unstructured":"Hajdu, \u00c1., T\u00f3th, T., V\u00f6r\u00f6s, A.: A survey on CEGAR-based model checking. Master\u2019s thesis, Budapest University of Technology and Economics (2015)"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.,\u00a0Jhala, R.,\u00a0Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 157\u2013171. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"11_CR34","unstructured":"ic3ia webpage. https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Ivrii, A., Nevo, Z., Baumgartner, J.: k-FAIR= k-LIVENESS+ FAIR revisiting SAT-based liveness algorithms. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20135. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602998"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Handbook of Model Checking, pp. 447\u2013491. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_15"},{"issue":"3","key":"11_CR37","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and model checking. In: Handbook of Model Checking, pp. 421\u2013446. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_14"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Turbo-charging lemmas on demand with don\u2019t care reasoning. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 179\u2013186. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987611"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 239\u2013251. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32\u201341. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), 15\u2013es (2007)","DOI":"10.1145\/1232420.1232422"},{"key":"11_CR43","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10703-006-0019-9","volume":"30","author":"T Schuele","year":"2007","unstructured":"Schuele, T., Schneider, K.: Bounded model checking of infinite state systems. Form. Methods Syst. Des. 30, 51\u201381 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"11_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-05089-3_7","volume-title":"FM 2009: Formal Methods","author":"S Tonetta","year":"2009","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 89\u2013105. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_7"},{"key":"11_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-662-49674-9_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Urban","year":"2016","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54\u201370. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_4"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure Versus Automata, pp. 238\u2013266 (2005)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Xia, Y., Cimatti, A., Griggio, A., Li, J.: Avoiding the shoals - a new approach to liveness checking. In: International Conference on Computer Aided Verification, pp. 234\u2013254. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_12"}],"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-98668-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:12:39Z","timestamp":1777302759000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","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","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}