{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:05Z","timestamp":1776333485211,"version":"3.51.2"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030451899","type":"print"},{"value":"9783030451905","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_4","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"58-76","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["A Calculus for Modular Loop Acceleration"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"4_CR1","unstructured":"Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis (2005), arXiv:cs\/0512056 [cs.MS]"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Acceleration from theory to practice. STTT 10(5), 401\u2013424 (2008). https:\/\/doi.org\/10.1007\/s10009-008-0064-3","DOI":"10.1007\/s10009-008-0064-3"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATVA\u00a0\u201905. pp. 474\u2013488. LNCS 3707 (2005). https:\/\/doi.org\/10.1007\/11562948_35","DOI":"10.1007\/11562948_35"},{"key":"4_CR4","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. Ph.D. thesis, Universit\u00e9 de Li\u00e8ge (1999), https:\/\/orbi.uliege.be\/bitstream\/2268\/74874\/1\/Boigelot98.pdf"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science 309(1-3), 413\u2013468 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(03)00314-1","DOI":"10.1016\/S0304-3975(03)00314-1"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: TACAS\u00a0\u201909. pp.337\u2013351. LNCS 5505 (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_29","DOI":"10.1007\/978-3-642-00768-2_29"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: CAV\u00a0\u201910. 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":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Deciding conditional termination. Logical Methods in Computer Science 10(3) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(3:8)2014","DOI":"10.2168\/LMCS-10(3:8)2014"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: CAV\u00a0\u201998. pp. 268\u2013279. LNCS 1427 (1998). https:\/\/doi.org\/10.1007\/BFb0028751","DOI":"10.1007\/BFb0028751"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD\u00a0\u201915. pp.57\u201364 (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: FMCAD\u00a0\u201919. pp. 221\u2013230 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894271","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration \u2013 artifact evaluation(2020). https:\/\/doi.org\/10.5281\/zenodo.3676348","DOI":"10.5281\/zenodo.3676348"},{"key":"4_CR13","unstructured":"Frohn, F.: A calculus for modular loop acceleration (2020), extended version, arXiv:2001.01516 [cs.LO]"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Frohn, F.: Empirical evaluation of \u201cA calculus for modular loopacceleration\u201d (2020), https:\/\/ffrohn.github.io\/acceleration-calculus","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Frohn, F., Hark, M., Giesl, J.: On the decidability of termination for polynomial loops (2019), arXiv:1910.11588 [cs.LO]","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Frohn, F., Naaf, M., Brockschmidt, M., Giesl, J.: Inferring lower runtime bounds for integer programs (2019), arXiv:1911.01077 [cs.LO]","DOI":"10.1145\/3410331"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: IJCAR\u00a0\u201916. pp. 550\u2013567. LNCS 9706 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_37","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Ganty, P., Iosif, R., Konecn\u00fd, F.: Underapproximation of procedure summaries for integer programs. STTT 19(5), 565\u2013584 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0420-7","DOI":"10.1007\/s10009-016-0420-7"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: TACAS\u00a0\u201919. 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":"4_CR20","doi-asserted-by":"publisher","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in line arrelation analysis. In: SAS\u00a0\u201906. pp. 144\u2013160. LNCS 4134 (2006). https:\/\/doi.org\/10.1007\/11823230_10","DOI":"10.1007\/11823230_10"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Science of Computer Programming 93, 125\u2013153 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.09.016","DOI":"10.1016\/j.scico.2013.09.016"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: POPL\u00a0\u201908. pp. 147\u2013158 (2008). https:\/\/doi.org\/10.1145\/1328438.1328459","DOI":"10.1145\/1328438.1328459"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Hojjat, H., Iosif, R., Konecn\u00fd, F., Kuncak, V., R\u00fcmmer, P.:Accelerating interpolants. In: ATVA\u00a0\u201912. pp. 187\u2013202. LNCS 7561 (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Hojjat, H., Konecn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems - tool paper. In: FM\u00a0\u201912. pp. 247\u2013251. LNCS 7436 (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_21","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL\u00a0\u201914. pp. 529\u2013540 (2014). https:\/\/doi.org\/10.1145\/2535838.2535843","DOI":"10.1145\/2535838.2535843"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI\u00a0\u201917. pp. 248\u2013262 (2017). https:\/\/doi.org\/10.1145\/3062341.3062373","DOI":"10.1145\/3062341.3062373"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Konecn\u00fd, F.: PTIME computation of transitive closures of octagonal relations. In: TACAS\u00a0\u201916. 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":"4_CR28","doi-asserted-by":"publisher","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. FMSD 47(1),75\u201392 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0228-1","DOI":"10.1007\/s10703-015-0228-1"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: FMCAD\u00a0\u201915. pp. 105\u2013111 (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542259","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Mourade Moura, L., Bj\u00f8rner, N.: An efficient SMT solver. In: TACAS \u201908. 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":"4_CR31","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: SODA\u00a0\u201915. pp. 957\u2013969 (2015). https:\/\/doi.org\/10.1137\/1.9781611973730.65","DOI":"10.1137\/1.9781611973730.65"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: CAV\u00a0\u201919. 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":"4_CR33","doi-asserted-by":"publisher","unstructured":"Strejcek, J., Trt\u00edk, M.: Abstracting path conditions. In: ISSTA\u00a0\u201912. pp.155\u2013165 (2012). https:\/\/doi.org\/10.1145\/2338965.2336772","DOI":"10.1145\/2338965.2336772"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: IJCAR\u00a0\u201914. pp. 367\u2013373. LNCS 8562(2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"4_CR35","unstructured":"Termination problems data base (TPDB), http:\/\/termination-portal.org\/wiki\/TPDB"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,9]],"date-time":"2021-03-09T08:52:26Z","timestamp":1615279946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}