{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:37Z","timestamp":1750220677465,"version":"3.41.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660,235950644"],"award-info":[{"award-number":["389792660,235950644"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,9,30]]},"abstract":"<jats:p>\n            We present a technique to infer\n            <jats:italic>lower<\/jats:italic>\n            bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce\n            <jats:italic>asymptotic<\/jats:italic>\n            lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.\n          <\/jats:p>","DOI":"10.1145\/3410331","type":"journal-article","created":{"date-parts":[[2020,10,15]],"date-time":"2020-10-15T22:12:21Z","timestamp":1602799941000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Inferring Lower Runtime Bounds for Integer Programs"],"prefix":"10.1145","volume":"42","author":[{"given":"Florian","family":"Frohn","sequence":"first","affiliation":[{"name":"Max Planck Institute for Informatics, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Naaf","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[{"name":"LuFG Informatik 2, RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Elvira Albert Diego E. Alonso-Blas Puri Arenas Samir Genaim and Germ\u00e1n Puebla. 2009. Asymptotic resource usage bounds. In APLAS\u201909 (LNCS 5904). 294--310.","DOI":"10.1007\/978-3-642-10672-9_21"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"e_1_2_1_5_1","first-page":"5","article-title":"Resource analysis driven by (conditional) termination proofs","volume":"19","author":"Albert Elvira","year":"2019","unstructured":"Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, and Albert Rubio. 2019. Resource analysis driven by (conditional) termination proofs. Theor. Pract. Log. Prog. 19, 5\u20136 (2019), 722--739.","journal-title":"Theor. Pract. Log. Prog."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Christophe Alias Alain Darte Paul Feautrier and Laure Gonnord. 2010. Multi-dimensional rankings program termination and complexity bounds of flowchart programs. In SAS\u201910 (LNCS 6337). 117--133.","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_1_7_1","volume-title":"Alonso-Blas and Samir Genaim","author":"Diego","year":"2012","unstructured":"Diego E. Alonso-Blas and Samir Genaim. 2012. On the limits of the classical approach to cost analysis. In SAS\u201912 (LNCS 7460). 405--421."},{"key":"e_1_2_1_8_1","volume-title":"PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs\/cs\/0512056","author":"Bagnara Roberto","year":"2005","unstructured":"Roberto Bagnara, Andrea Pescetti, Alessandro Zaccagnini, and Enea Zaffanella. 2005. PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs\/cs\/0512056 (2005)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_2_1_10_1","volume-title":"ABC: Algebraic bound computation for loops. In LPAR\u201910 (LNCS 6355). 103--118.","author":"Blanc R\u00e9gis","year":"2010","unstructured":"R\u00e9gis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kov\u00e1cs. 2010. ABC: Algebraic bound computation for loops. In LPAR\u201910 (LNCS 6355). 103--118."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Marius Bozga Codruta G\u00eerlea and Radu Iosif. 2009. Iterating octagons. In TACAS\u201909 (LNCS 5505). 337--351.","DOI":"10.1007\/978-3-642-00768-2_29"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Marius Bozga Radu Iosif and Filip Konecn\u00fd. 2010. Fast acceleration of ultimately periodic relations. In CAV\u201910 (LNCS 6174). 227--242.","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"e_1_2_1_13_1","volume-title":"Sipma","author":"Bradley Aaron R.","year":"2005","unstructured":"Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear ranking with reachability. In CAV\u201905 (LNCS 3576). 491--504."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_2_1_15_1","volume-title":"WISE: Automated test generation for worst-case complexity. In ICSE\u201909. 463--473.","author":"Burnim Jacob","year":"2009","unstructured":"Jacob Burnim, Sudeep Juvekar, and Koushik Sen. 2009. WISE: Automated test generation for worst-case complexity. In ICSE\u201909. 463--473."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Pavel Cadek Clemens Danninger Moritz Sinn and Florian Zuleger. 2018. Using loop bound analysis for invariant generation. In FMCAD\u201918. 1--9.","DOI":"10.23919\/FMCAD.2018.8603005"},{"key":"e_1_2_1_18_1","unstructured":"Peter Cameron. 2017. Polynomials Taking Integer Values. Retrieved from https:\/\/cameroncounts.wordpress.com\/2017\/01\/31\/polynomials-taking-integer-values\/."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann and Zhong Shao. 2015. Compositional certified resource bounds. In PLDI\u201915. 467--478.","DOI":"10.1145\/2813885.2737955"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann Thomas W. Reps and Zhong Shao. 2017. Automated resource analysis with Coq proof objects. In CAV\u201917 (LNCS 10427). 64--85.","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS\u201908 (LNCS 4963). 337--340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_22_1","unstructured":"Saumya Debray Pedro L\u00f3pez-Garc\u00eda Manuel V. Hermenegildo and Nai-Wei Lin. 1997. Lower bound cost estimation for logic programs. In ILPS\u201997. 291--305."},{"key":"e_1_2_1_23_1","unstructured":"Complexity Analysis-Based Guaranteed Execution. 2015. Retrieved from https:\/\/www.draper.com\/news-releases\/drapers-cage-could-spot-code-vulnerable-denial-service-attacks."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Stephan Falke Deepak Kapur and Carsten Sinz. 2012. Termination analysis of imperative programs using bitvector arithmetic. In VSTTE\u201912 (LNCS 7152). 261--277.","DOI":"10.1007\/978-3-642-27705-4_21"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional recurrence analysis. In FMCAD\u201915. 57--64.","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Antonio Flores-Montoya and Reiner H\u00e4hnle. 2014. Resource analysis of complex programs with cost equations. In APLAS\u201914 (LNCS 8858). 275--295.","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Antonio Flores-Montoya. 2016. Upper and lower amortized cost bounds of programs expressed as cost relations. In FM\u201916 (LNCS 9995). 254--273.","DOI":"10.1007\/978-3-319-48989-6_16"},{"key":"e_1_2_1_28_1","unstructured":"Space\/Time Analysis for Cybersecurity (STAC). 2015. Retrieved from http:\/\/www.darpa.mil\/program\/space-time-analysis-for-cybersecurity."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Florian Frohn Matthias Naaf Jera Hensel Marc Brockschmidt and J\u00fcrgen Giesl. 2016. Lower runtime bounds for integer programs. In IJCAR\u201916 (LNAI 9706). 550--567.","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9397-x"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Florian Frohn and J\u00fcrgen Giesl. 2019. Termination of triangular integer loops is decidable. In CAV\u201919 (LNCS 11562). 426--444.","DOI":"10.1007\/978-3-030-25543-5_24"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Florian Frohn and J\u00fcrgen Giesl. 2019. Proving non-termination via loop acceleration. In FMCAD\u201919. 221--230.","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Florian Frohn Matthias Naaf Marc Brockschmidt and J\u00fcrgen Giesl. 2020. Empirical Evaluation of \u201cInferring Lower Runtime Bounds for Integer Programs.\u201d Retrieved from https:\/\/aprove-developers.github.io\/its-lowerbounds-journal.","DOI":"10.1145\/3410331"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of nondeterministic probabilistic programs. In VMCAI\u201919 (LNCS 11388). 468--490.","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0420-7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Giesl Peter Giesl and Marcel Hark. 2019. Computing expected runtimes for constant probability programs. In CADE\u201919 (LNAI 11716). 269--286.","DOI":"10.1007\/978-3-030-29436-6_16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In TACAS\u201919 (LNCS 11429). 156--166.","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Laure Gonnord and Nicolas Halbwachs. 2006. Combining widening and acceleration in linear relation analysis. In SAS\u201906 (LNCS 4134). 144--160.","DOI":"10.1007\/11823230_10"},{"key":"e_1_2_1_39_1","volume-title":"Chilimbi","author":"Gulwani Sumit","year":"2009","unstructured":"Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: Precise and efficient static estimation of program computational complexity. In POPL\u201909. 127--139."},{"key":"e_1_2_1_40_1","volume-title":"J\u00fcrgen Giesl, and Joost-Pieter Katoen.","author":"Hark Marcel","year":"2020","unstructured":"Marcel Hark, Benjamin Lucien Kaminski, J\u00fcrgen Giesl, and Joost-Pieter Katoen. 2020. Aiming low is harder\u2014Inductive proof rules for lower bounds on weakest preexpectations in probabilistic program verification. PACMPL 4, POPL (2020), 37:1--37:28."},{"key":"e_1_2_1_41_1","volume-title":"Introduction to Maple","author":"Heck Andr\u00e9","unstructured":"Andr\u00e9 Heck. 1996. Introduction to Maple (2nd ed.). Springer.","edition":"2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.02.004"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Nao Hirokawa and Georg Moser. 2008. Automated complexity analysis based on the dependency pair method. In IJCAR\u201908 (LNAI 5195). 364--379.","DOI":"10.1007\/978-3-540-71070-7_32"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Dieter Hofbauer and Clemens Lautemann. 1989. Termination proofs and the length of derivations. In RTA\u201989 (LNCS 355). 167--177.","DOI":"10.1007\/3-540-51081-8_107"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_1_46_1","volume-title":"Type-based amortized resource analysis with integers and arrays. J. Funct. Prog. 25","author":"Hoffmann Jan","year":"2015","unstructured":"Jan Hoffmann and Zhong Shao. 2015. Type-based amortized resource analysis with integers and arrays. J. Funct. Prog. 25 (2015)."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In POPL\u201917. 359--373.","DOI":"10.1145\/3093333.3009842"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Bertrand Jeannet Peter Schrammel and Sriram Sankaranarayanan. 2014. Abstract acceleration of general linear loops. In POPL\u201914. 529--540.","DOI":"10.1145\/2578855.2535843"},{"key":"e_1_2_1_49_1","unstructured":"KoAT Benchmarks 2014. Retrieved from https:\/\/github.com\/s-falke\/kittel-koat\/tree\/master\/koat-evaluation\/examples."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0228-1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Daniel Larraz Albert Oliveras Enric Rodr\u00edguez-Carbonell and Albert Rubio. 2013. Proving termination of imperative programs using Max-SMT. In FMCAD\u201913. 218--225.","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"e_1_2_1_52_1","unstructured":"LoAT. 2019. Retrieved from https:\/\/github.com\/aprove-developers\/LoAT."},{"key":"e_1_2_1_53_1","volume-title":"Srivas","author":"Madhukar Kumar","year":"2015","unstructured":"Kumar Madhukar, Bj\u00f6rn Wachter, Daniel Kroening, Matt Lewis, and Mandayam K. Srivas. 2015. Accelerating invariant generation. In FMCAD\u201915. 105--111."},{"volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","key":"e_1_2_1_54_1","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_55_1","doi-asserted-by":"crossref","unstructured":"Matthias Naaf Florian Frohn Marc Brockschmidt Carsten Fuhs and J\u00fcrgen Giesl. 2017. Complexity analysis for term rewriting by integer transition systems. In FroCoS\u201917 (LNAI 10483). 132--150.","DOI":"10.1007\/978-3-319-66167-4_8"},{"key":"e_1_2_1_56_1","doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In VMCAI\u201904 (LNCS 2937). 239--251.","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"e_1_2_1_58_1","volume-title":"Harris","author":"Srikanth Akhilesh","year":"2017","unstructured":"Akhilesh Srikanth, Burak Sahin, and William R. Harris. 2017. Complexity verification using guided theorem enumeration. In POPL\u201917. 639--652."},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Jan Strejcek and Marek Trt\u00edk. 2012. Abstracting path conditions. In ISSTA\u201912. 155--165.","DOI":"10.1145\/2338965.2336772"},{"key":"e_1_2_1_60_1","volume-title":"POPL","author":"Wang Di","year":"2019","unstructured":"Di Wang and Jan Hoffmann. 2019. Type-guided worst-case input generation. PACMPL 3, POPL (2019), 13:1--13:30."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1137\/1034112"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3410331","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3410331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:15Z","timestamp":1750197795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3410331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":61,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,9,30]]}},"alternative-id":["10.1145\/3410331"],"URL":"https:\/\/doi.org\/10.1145\/3410331","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"2019-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}