{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:52:31Z","timestamp":1781927551345,"version":"3.54.5"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","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,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"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                    We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by\n                    <jats:italic>transitive relations<\/jats:italic>\n                    until its\n                    <jats:italic>diameter<\/jats:italic>\n                    <jats:italic>D<\/jats:italic>\n                    becomes finite, i.e., until constantly\u00a0many steps suffice to cover all reachable states, irrespective of\u00a0the initial state. Then we can prove safety by checking that no error state is reachable in\n                    <jats:italic>D<\/jats:italic>\n                    steps. To deduce transitive relations, we use\n                    <jats:italic>recurrence analysis<\/jats:italic>\n                    . While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with\n                    <jats:italic>projections<\/jats:italic>\n                    . An empirical evaluation of the implementation of our approach in our tool  shows that it is highly competitive with the state of the art.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_25","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:52Z","timestamp":1753789672000},"page":"468-489","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Infinite State Model Checking by\u00a0Learning Transitive Relations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATVA\u00a02005, pp. 474\u2013488. LNCS 3707 (2005). https:\/\/doi.org\/10.1007\/11562948_35","DOI":"10.1007\/11562948_35"},{"key":"25_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"25_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"25_CR4","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn solver. In: CAV\u00a02023, pp. 209\u2013223. LNCS 13965 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"25_CR5","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: CAV\u00a02010, pp. 227\u2013242. LNCS 6174 (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"25_CR6","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI 2011, pp. 70\u201387. LNCS 6538 (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"issue":"1","key":"25_CR7","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/PL00009410","volume":"21","author":"D Bremner","year":"1999","unstructured":"Bremner, D.: Incremental convex hull algorithms are not output sensitive. Discret. Comput. Geom. 21(1), 57\u201368 (1999). https:\/\/doi.org\/10.1007\/PL00009410","journal-title":"Discret. Comput. Geom."},{"key":"25_CR8","doi-asserted-by":"publisher","unstructured":"Britikov, K., Blicha, M., Sharygina, N., Fedyukovich, G.: Reachability analysis for multiloop programs using transition power abstraction. In: FM\u00a02024, pp. 558\u2013576. LNCS 14933 (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_29","DOI":"10.1007\/978-3-031-71162-6_29"},{"key":"25_CR9","unstructured":"CHC Competition, https:\/\/chc-comp.github.io"},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV\u00a02000, pp. 154\u2013169. LNCS 1855 (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"25_CR11","first-page":"91","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u201399 (1972)","journal-title":"Mach. Intell."},{"key":"25_CR12","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: CAV\u00a02014, pp. 737\u2013744. LNCS 8559 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"25_CR13","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (1972)"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD\u00a02015, pp. 57\u201364 (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: TACAS\u00a02020, pp. 58\u201376. LNCS 12078 (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"25_CR16","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: IJCAR\u00a02022, pp. 712\u2013722. LNCS 13385 (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"25_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination by acceleration driven clause learning. In: CADE\u00a02023, pp. 220\u2013233. LNCS 14132 (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_13","DOI":"10.1007\/978-3-031-38499-8_13"},{"key":"25_CR18","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: ADCL: acceleration driven clause learning for constrained Horn clauses. In: SAS\u00a02023, pp. 259\u2013285. LNCS 14284 (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_13","DOI":"10.1007\/978-3-031-44245-2_13"},{"key":"25_CR19","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Integrating loop acceleration into bounded model checking. In: FM\u00a02024, pp. 73\u201391. LNCS 14933 (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_4","DOI":"10.1007\/978-3-031-71162-6_4"},{"key":"25_CR20","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Infinite state model checking by learning transitive relations. CoRR abs\/2502.04761 (2025). https:\/\/doi.org\/10.48550\/arXiv.2502.04761","DOI":"10.48550\/arXiv.2502.04761"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Evaluation of \u201cInfinite State Model Checking by Learning Transitive Relations\u201d (2025), https:\/\/loat-developers.github.io\/trl-eval\/","DOI":"10.1007\/978-3-031-99984-0_25"},{"key":"25_CR22","unstructured":"Frohn, F., Giesl, J.: LoAT website, https:\/\/loat-developers.github.io\/LoAT\/"},{"key":"25_CR23","unstructured":"Genov, B.: The convex hull problem in practice: improving the running time of the double description method. Ph.D. thesis, Bremen University, Germany (2015), https:\/\/media.suub.uni-bremen.de\/handle\/elib\/833"},{"key":"25_CR24","doi-asserted-by":"publisher","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: TACAS\u00a02019, pp. 156\u2013166. LNCS 11429 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"25_CR25","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV\u00a01997, pp. 72\u201383. LNCS 1254 (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"25_CR26","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica Horn solver. In: FMCAD\u00a02018, pp.\u00a01\u20137 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"25_CR27","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: FMCAD\u00a02016, pp. 85\u201392 (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886665","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"25_CR28","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI\u00a02017, pp. 248\u2013262 (2017). https:\/\/doi.org\/10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"issue":"3","key":"25_CR29","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":"25_CR30","doi-asserted-by":"publisher","unstructured":"Kone\u010dn\u00fd, F.: PTIME computation of transitive closures of octagonal relations. In: TACAS\u00a02016, pp. 645\u2013661. LNCS 9636 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_42","DOI":"10.1007\/978-3-662-49674-9_42"},{"key":"25_CR31","doi-asserted-by":"publisher","unstructured":"Krishnan, H.G.V., Chen, Y., Shoham, S., Gurfinkel, A.: Global guidance for local generalization in model checking. In: CAV\u00a02020, pp. 101\u2013125. LNCS 12225 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_7","DOI":"10.1007\/978-3-030-53291-8_7"},{"issue":"3","key":"25_CR32","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/S10703-012-0176-Y","volume":"42","author":"D Kroening","year":"2013","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using state and transition invariants. Formal Methods Syst. Des. 42(3), 221\u2013261 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0176-Y","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR33","doi-asserted-by":"publisher","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Proving safety with trace automata and bounded model checking. In: FM\u00a02015, pp. 325\u2013341. LNCS 9109 (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_21","DOI":"10.1007\/978-3-319-19249-9_21"},{"key":"25_CR34","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV\u00a02003, pp. 1\u201313. LNCS 2725 (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"25_CR35","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV\u00a02006, pp. 123\u2013136. LNCS 4144 (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"25_CR36","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS 2008, pp. 337\u2013340. LNCS 4963 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"25_CR37","doi-asserted-by":"publisher","unstructured":"Pimpalkhare, N., Kincaid, Z.: Semi-linear VASR for over-approximate semi-linear transition system reachability. In: RP\u00a02024, pp. 154\u2013166. LNCS 15050 (2024). https:\/\/doi.org\/10.1007\/978-3-031-72621-7_11","DOI":"10.1007\/978-3-031-72621-7_11"},{"key":"25_CR38","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS\u00a02004, pp. 32\u201341 (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319598","DOI":"10.1109\/LICS.2004.1319598"},{"key":"25_CR39","doi-asserted-by":"publisher","unstructured":"Promies, V., \u00c1brah\u00e1m, E.: A divide-and-conquer approach to variable elimination in linear real arithmetic. In: FM\u00a02024, pp. 131\u2013148. LNCS 14933 (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_7","DOI":"10.1007\/978-3-031-71162-6_7"},{"key":"25_CR40","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: FMCAD\u00a02000, pp. 108\u2013125. LNCS 1954 (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"25_CR41","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: CAV\u00a02019, pp. 97\u2013115. LNCS 11562 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"25_CR42","doi-asserted-by":"publisher","unstructured":"Solanki, M., Chatterjee, P., Lal, A., Roy, S.: Accelerated bounded model checking using interpolation based summaries. In: TACAS\u00a02024, pp. 155\u2013174. LNCS 14571 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_8","DOI":"10.1007\/978-3-031-57249-4_8"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:25:34Z","timestamp":1781882734000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_25","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":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}