{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:58:50Z","timestamp":1782867530975,"version":"3.54.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-032-22749-2_7","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:13:30Z","timestamp":1776258810000},"page":"131-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Deciding Constant Runtime of Linear Loops"],"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1421-6980","authenticated-orcid":false,"given":"Peter","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3187-9217","authenticated-orcid":false,"given":"Nils","family":"Lommen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Akshay, S., Balaji, N., Vyas, N.: Complexity of restricted variants of Skolem and related problems. In: Proc. MFCS\u00a0\u201917. LIPIcs 83 (2017). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2017.78","DOI":"10.4230\/LIPICS.MFCS.2017.78"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Albert, E., Bofill, M., Borralleras, C., Mart\u00edn-Mart\u00edn, E., Rubio, A.: Resource analysis driven by (conditional) termination proofs. Theory and Practice of Logic Programming 19(5\u20136), 722\u2013739 (2019). https:\/\/doi.org\/10.1017\/S1471068419000152","DOI":"10.1017\/S1471068419000152"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Albert, E., Genaim, S., Mart\u00edn-Mart\u00edn, E., Merayo, A., Rubio, A.: Lower-bound synthesis using loop specialization and Max-SMT. In: Proc. CAV\u00a0\u201921. pp. 863\u2013886. LNCS 12760 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_40","DOI":"10.1007\/978-3-030-81688-9_40"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Proc. CAV\u00a0\u201917. pp. 601\u2013620. LNCS 10427 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M., Dom\u00e9nech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Proc. SAS\u00a0\u201919. pp. 459\u2013480. LNCS 11822 (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_22","DOI":"10.1007\/978-3-030-32304-2_22"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Bogart, T., Goodrick, J., Woods, K.: Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior. Discrete Analysis (2017). https:\/\/doi.org\/10.19086\/da.1254","DOI":"10.19086\/da.1254"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Braverman, M.: Termination of integer linear programs. In: Proc. CAV\u00a0\u201906. pp. 372\u2013385. LNCS 4144 (2006). https:\/\/doi.org\/10.1007\/11817963_34","DOI":"10.1007\/11817963_34"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Cai, J.Y.: Computing Jordan normal forms exactly for commuting matrices in polynomial time. International Journal of Foundations of Computer Science 5(3\/4), 293\u2013302 (1994). https:\/\/doi.org\/10.1142\/S0129054194000165","DOI":"10.1142\/S0129054194000165"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Proc. FM\u00a0\u201916. pp. 254\u2013273. LNCS 9995 (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_16","DOI":"10.1007\/978-3-319-48989-6_16"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: Proc. CAV\u00a0\u201919. pp. 426\u2013444. LNCS 11562 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24","DOI":"10.1007\/978-3-030-25543-5_24"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Proc. TACAS\u00a0\u201920. 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":"7_CR12","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with\u00a0LoAT (System description). In: Proc. IJCAR\u00a0\u201922. 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":"7_CR13","doi-asserted-by":"publisher","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Proc. TACAS\u00a0\u201919. pp. 156\u2013166. LNCS 11429 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10, website of TermComp: https:\/\/termination-portal.org\/wiki\/Termination_Competition","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Hark, M., Frohn, F., Giesl, J.: Polynomial loops: Beyond termination. In: Proc. LPAR\u00a0\u201920. pp. 279\u2013297. EPiC 73 (2020). https:\/\/doi.org\/10.29007\/NXV1","DOI":"10.29007\/NXV1"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Hark, M., Frohn, F., Giesl, J.: Termination of triangular polynomial loops. Formal Methods in System Design 65(1), 70\u2013132 (2025). https:\/\/doi.org\/10.1007\/s10703-023-00440-z","DOI":"10.1007\/s10703-023-00440-z"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Das, A., Weng, S.: Towards automatic resource bound analysis for OCaml. In: Proc. POPL\u00a0\u201917. pp. 359\u2013373 (2017). https:\/\/doi.org\/10.1145\/3009837.3009842","DOI":"10.1145\/3009837.3009842"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Hosseini, M., Ouaknine, J., Worrell, J.: Termination of linear loops over the integers. In: Proc. ICALP\u00a0\u201919. LIPIcs 132 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.118","DOI":"10.4230\/LIPIcs.ICALP.2019.118"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Cyphert, J., Reps, T.: Closed forms for numerical loops. Proceedings of the ACM on Programming Languages 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290368","DOI":"10.1145\/3290368"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L.: A complete invariant generation approach for P-solvable loops. In: Proc. PSI\u00a0\u201909. pp. 242\u2013256. LNCS 5947 (2010). https:\/\/doi.org\/10.1007\/978-3-642-11486-1_21","DOI":"10.1007\/978-3-642-11486-1_21"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Lommen, N., Meyer, F., Giesl, J.: Automatic complexity analysis of integer programs via triangular weakly non-linear loops. In: Proc. IJCAR\u00a0\u201922. pp. 734\u2013754. LNCS 13385 (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_43","DOI":"10.1007\/978-3-031-10769-6_43"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Lommen, N., Giesl, J.: Targeting completeness: Using closed forms for size bounds of integer programs. In: Proc. FroCoS\u00a0\u201923. pp. 3\u201322. LNCS 14279 (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_1","DOI":"10.1007\/978-3-031-43369-6_1"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Loopy: Artifact, Evaluation, and Benchmarks. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.17313899","DOI":"10.5281\/zenodo.17313899"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Mansutti, A., Starchak, M.R.: One-parametric Presburger arithmetic has quantifier elimination. In: Proc. MFCS\u00a0\u201925. LIPIcs\u00a0345 (2025). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2025.72","DOI":"10.4230\/LIPICS.MFCS.2025.72"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Meurer, A., Smith, C.P., Paprocki, M., \u010cert\u00edk, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., Rathnayake, T., Vig, S., Granger, B.E., Muller, R.P., Bonazzi, F., Gupta, H., Vats, S., Johansson, F., Pedregosa, F., Curry, M.J., Terrel, A.R., Rou\u010dka, \u0160., Saboo, A., Fernando, I., Kulal, S., Cimrman, R., Scopatz, A.: SymPy: symbolic computing in Python. PeerJ Computer Science 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","DOI":"10.7717\/peerj-cs.103"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Proc. SODA\u00a0\u201915. pp. 957\u2013969 (2015). https:\/\/doi.org\/10.1137\/1.9781611973730.65","DOI":"10.1137\/1.9781611973730.65"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"P\u00f3lya, G., Szeg\u00f6, G.: Problems and Theorems in Analysis II: Theory of Functions. Zeros. Polynomials. Determinants. Number Theory. Geometry. Classics in Mathematics, Springer (1976). https:\/\/doi.org\/10.1007\/978-3-642-61905-2","DOI":"10.1007\/978-3-642-61905-2"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. Journal of Automated Reasoning 59(1), 3\u201345 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9402-4","DOI":"10.1007\/s10817-016-9402-4"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Tiwari, A.: Termination of linear programs. In: Proc. CAV\u00a0\u201904. pp. 70\u201382. LNCS 3114 (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"7_CR29","unstructured":"TPDB (Termination Problems Data Base), https:\/\/github.com\/TermCOMP\/TPDB"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Xu, M., Li, Z.B.: Symbolic termination analysis of solvable loops. Journal of Symbolic Computation 50, 28\u201349 (2013). https:\/\/doi.org\/10.1016\/j.jsc.2012.05.005","DOI":"10.1016\/j.jsc.2012.05.005"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:35:57Z","timestamp":1782866157000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_7","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":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"An artifact including our implementation in the tool\n                      Loopy\n                      is available at [\n                      \n                      ]:\n                      \n                      This artifact allows to reproduce all results of our evaluation.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability Statement"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}