{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:51Z","timestamp":1775868591615,"version":"3.50.1"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031081651","type":"print"},{"value":"9783031081668","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_10","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"193-228","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Improving Automatic Complexity Analysis of\u00a0Integer Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3187-9217","authenticated-orcid":false,"given":"Nils","family":"Lommen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-3177","authenticated-orcid":false,"given":"Marcel","family":"Hark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1038-4944","authenticated-orcid":false,"given":"Fabian","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-69166-2_15","volume-title":"Static Analysis","author":"E Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221\u2013237. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_15"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2011.07.009","volume":"413","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142\u2013159 (2012). https:\/\/doi.org\/10.1016\/j.tcs.2011.07.009","journal-title":"Theor. Comput. Sci."},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3), 22:1\u201322:35 (2013). https:\/\/doi.org\/10.1145\/2499937.2499943","DOI":"10.1145\/2499937.2499943"},{"issue":"4","key":"10_CR5","doi-asserted-by":"publisher","first-page":"987","DOI":"10.1007\/s10270-015-0476-y","volume":"15","author":"E Albert","year":"2015","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: A formal verification framework for static analysis. Softw. Syst. Model. 15(4), 987\u20131012 (2015). https:\/\/doi.org\/10.1007\/s10270-015-0476-y","journal-title":"Softw. Syst. Model."},{"issue":"5\u20136","key":"10_CR6","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1017\/S1471068419000152","volume":"19","author":"E Albert","year":"2019","unstructured":"Albert, E., Bofill, M., Borralleras, C., Mart\u00edn-Mart\u00edn, E., Rubio, A.: Resource analysis driven by (conditional) termination proofs. Theory Pract. Log. Program. 19(5\u20136), 722\u2013739 (2019). https:\/\/doi.org\/10.1017\/S1471068419000152","journal-title":"Theory Pract. Log. Program."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-030-81688-9_40","volume-title":"Computer Aided Verification","author":"E Albert","year":"2021","unstructured":"Albert, E., Genaim, S., Martin-Martin, E., Merayo, A., Rubio, A.: Lower-bound synthesis using loop specialization and Max-SMT. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 863\u2013886. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_40"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G.: A combination framework for complexity. In: van Raamsdonk, F. (ed.) RTA 2013. LIPIcs, vol. 21, pp. 55\u201370. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.55","DOI":"10.4230\/LIPIcs.RTA.2013.55"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-662-49674-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Avanzini","year":"2016","unstructured":"Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean complexity tool. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 407\u2013423. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_24"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1\u201326:55 (2014). https:\/\/doi.org\/10.1145\/2629488","DOI":"10.1145\/2629488"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/978-3-319-63390-9_32","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2017","unstructured":"Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 601\u2013620. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-030-32304-2_22","volume-title":"Static Analysis","author":"AM Ben-Amram","year":"2019","unstructured":"Ben-Amram, A.M., Dom\u00e9nech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 459\u2013480. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_22"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-54577-5_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Borralleras","year":"2017","unstructured":"Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 99\u2013117. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_6"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1007\/11523468_109","volume-title":"Automata, Languages and Programming","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349\u20131361. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11523468_109"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4), 13:1\u201313:50 (2016). https:\/\/doi.org\/10.1145\/2866575","DOI":"10.1145\/2866575"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S.M. (eds.) PLDI 2015, pp. 467\u2013478 (2015). https:\/\/doi.org\/10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"10_CR18","unstructured":"Clang Compiler. https:\/\/clang.llvm.org\/"},{"key":"10_CR19","unstructured":"Dom\u00e9nech, J.J., Genaim, S.: \u201ciRankFinder\u201d. In: Lucas, S. (ed.) WST 2018, p. 83 (2018). http:\/\/wst2018.webs.upv.es\/wst2018proceedings.pdf"},{"issue":"5\u20136","key":"10_CR20","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1017\/S1471068419000310","volume":"19","author":"JJ Dom\u00e9nech","year":"2019","unstructured":"Dom\u00e9nech, J.J., Gallagher, J.P., Genaim, S.: Control-flow refinement by partial evaluation, and its application to termination and cost analysis. Theory Pract. Log. Program. 19(5\u20136), 990\u20131005 (2019). https:\/\/doi.org\/10.1017\/S1471068419000310","journal-title":"Theory Pract. Log. Program."},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schauss, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 41\u201350. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.41","DOI":"10.4230\/LIPIcs.RTA.2011.41"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-12736-1_15","volume-title":"Programming Languages and Systems","author":"A Flores-Montoya","year":"2014","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275\u2013295. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12736-1_15"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-319-48989-6_16","volume-title":"FM 2016: Formal Methods","author":"A Flores-Montoya","year":"2016","unstructured":"Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 254\u2013273. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_16"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-66845-1_6","volume-title":"Integrated Formal Methods","author":"F Frohn","year":"2017","unstructured":"Frohn, F., Giesl, J.: Complexity analysis for Java with AProVE. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 85\u2013101. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_6"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10817-016-9397-x","volume":"59","author":"F Frohn","year":"2016","unstructured":"Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Str\u00f6der, T.: Lower bounds for runtime complexity of term rewriting. J. Autom. Reason. 59(1), 121\u2013163 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9397-x","journal-title":"J. Autom. Reason."},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Barrett, C.W., Yang, J. (eds.) FMCAD 2019, pp. 221\u2013230 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894271","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Frohn, F., Naaf, M., Brockschmidt, M., Giesl, J.: Inferring lower runtime bounds for integer programs. ACM Trans. Program. Lang. Syst. 42(3), 13:1\u201313:50 (2020). https:\/\/doi.org\/10.1145\/3410331","DOI":"10.1145\/3410331"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Gallagher, J.P.: Polyvariant program specialisation with property-based abstraction. In: VPT@Programming. EPTCS, vol. 299, pp. 34\u201348 (2019). https:\/\/doi.org\/10.4204\/EPTCS.299.6","DOI":"10.4204\/EPTCS.299.6"},{"issue":"1","key":"10_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2016","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J. Autom. Reason."},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-030-29436-6_16","volume-title":"Automated Deduction \u2013 CADE 27","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 269\u2013286. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-030-17502-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012). https:\/\/doi.org\/10.1145\/2362389.2362393","DOI":"10.1145\/2362389.2362393"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 359\u2013373 (2017). https:\/\/doi.org\/10.1145\/3009837.3009842","DOI":"10.1145\/3009837.3009842"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C.: Expected runtime analysis by program verification. In: Barthe, G., Katoen, J.-P., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 185\u2013220. Cambridge University Press (2020). https:\/\/doi.org\/10.1017\/9781108770750.007","DOI":"10.1017\/9781108770750.007"},{"key":"10_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18490-1","volume-title":"Analysis 1","author":"K K\u00f6nigsberger","year":"2004","unstructured":"K\u00f6nigsberger, K.: Analysis 1, 6th edn. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-642-18490-1","edition":"6"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75\u201388. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"10_CR38","doi-asserted-by":"publisher","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:16)2015","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"10_CR40","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.ic.2018.05.007","volume":"261","author":"G Moser","year":"2018","unstructured":"Moser, G., Schaper, M.: From Jinja bytecode to term rewriting: a complexity reflecting transformation. Inf. Comput. 261, 116\u2013143 (2018). https:\/\/doi.org\/10.1016\/j.ic.2018.05.007","journal-title":"Inf. Comput."},{"key":"10_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR42","unstructured":"KoAT: Web Interface, Experiments, Source Code, Binary, and Docker Image. https:\/\/aprove-developers.github.io\/ComplexityMprfCfr\/"},{"issue":"1","key":"10_CR43","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s10817-013-9277-6","volume":"51","author":"L Noschinski","year":"2013","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27\u201356 (2013). https:\/\/doi.org\/10.1007\/s10817-013-9277-6","journal-title":"J. Autom. Reason."},{"key":"10_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"10_CR45","unstructured":"RaML (Resource Aware ML). https:\/\/www.raml.co\/interface\/"},{"issue":"1","key":"10_CR46","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3\u201345 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9402-4","journal-title":"J. Autom. Reason."},{"key":"10_CR47","doi-asserted-by":"publisher","unstructured":"Srikanth, A., Sahin, B., Harris, W.R.: Complexity verification using guided theorem enumeration. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 639\u2013652 (2017). https:\/\/doi.org\/10.1145\/3009837.3009864","DOI":"10.1145\/3009837.3009864"},{"key":"10_CR48","unstructured":"TPDB (Termination Problems Data Base). https:\/\/github.com\/TermCOMP\/TPDB"},{"key":"10_CR49","doi-asserted-by":"publisher","unstructured":"Wang, D., Hoffmann, J.: Type-guided worst-case input generation. Proc. ACM Program. Lang. 3(POPL), 13:1\u201313:30 (2019). https:\/\/doi.org\/10.1145\/3290326","DOI":"10.1145\/3290326"},{"issue":"1","key":"10_CR50","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s10009-019-00527-1","volume":"23","author":"Y Yuan","year":"2019","unstructured":"Yuan, Y., Li, Y., Shi, W.: Detecting multiphase linear ranking functions for single-path linear-constraint loops. Int. J. Softw. Tools Technol. Transfer 23(1), 55\u201367 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00527-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:38:15Z","timestamp":1656891495000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}