{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:52:26Z","timestamp":1775868746620,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661667","type":"print"},{"value":"9783319661674","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_8","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:15:18Z","timestamp":1503918918000},"page":"132-150","source":"Crossref","is-referenced-by-count":11,"title":["Complexity Analysis for Term Rewriting by Integer Transition Systems"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Naaf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161\u2013203 (2011)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"8_CR2","doi-asserted-by":"crossref","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. Sc. 413(1), 142\u2013159 (2012)","journal-title":"Theor. Comput. Sc."},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-319-14125-1_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"E Albert","year":"2014","unstructured":"Albert, E., Genaim, S., Guti\u00e8rrez, R.: A transformational approach to resource analysis with typed-norms. In: Gupta, G., Pe\u00f1a, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 38\u201353. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-14125-1_3"},{"key":"8_CR4","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). doi: 10.1007\/978-3-642-15769-1_8"},{"key":"8_CR5","unstructured":"AProVE. https:\/\/aprove-developers.github.io\/trs_complexity_via_its\/"},{"key":"8_CR6","unstructured":"Avanzini, M., Felgenhauer, B.: Type introduction for runtime complexity analysis. In: WST 2014, pp. 1\u20135 (2014). http:\/\/www.easychair.org\/smart-program\/VSL2014\/WST-proceedings.pdf"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Berlin, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_24"},{"key":"8_CR8","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.ic.2015.12.007","volume":"248","author":"M Avanzini","year":"2016","unstructured":"Avanzini, M., Moser, G.: A combination framework for complexity. Inform. Comput. 248, 22\u201355 (2016)","journal-title":"Inform. Comput."},{"key":"8_CR9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge U. Press, Cambridge (1998)"},{"issue":"4","key":"8_CR10","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1017\/S0960129511000685","volume":"22","author":"P Baillot","year":"2012","unstructured":"Baillot, P., Dal Lago, U., Moyen, J.Y.: On quasi-interpretations, blind abstractions and implicit complexity. Math. Struct. Compt. Sci. 22(4), 549\u2013580 (2012)","journal-title":"Math. Struct. Compt. Sci."},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-17511-4_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Blanc","year":"2010","unstructured":"Blanc, R., Henzinger, T.A., Hottelier, T., Kov\u00e0cs, L.: ABC: Algebraic bound computation for loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 103\u2013118. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_7"},{"issue":"1","key":"8_CR12","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0956796800003877","volume":"11","author":"G Bonfante","year":"2001","unstructured":"Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Program. 11(1), 33\u201353 (2001)","journal-title":"J. Funct. Program."},{"issue":"4","key":"8_CR13","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/2866575","volume":"38","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM TOPLAS 38(4), 13 (2016)","journal-title":"ACM TOPLAS"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: PLDI 2015, pp. 467\u2013478 (2015)","DOI":"10.1145\/2737924.2737955"},{"issue":"5","key":"8_CR15","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/161468.161472","volume":"15","author":"S Debray","year":"1993","unstructured":"Debray, S., Lin, N.: Cost analysis of logic programs. TOPLAS 15(5), 826\u2013875 (1993)","journal-title":"TOPLAS"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"550","DOI":"10.1007\/978-3-319-40229-1_37","volume-title":"Automated Reasoning","author":"F Frohn","year":"2016","unstructured":"Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 550\u2013567. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_37"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Analyzing runtime complexity via innermost runtime complexity. In: LPAR 2017, pp. 249\u2013268 (2017)","DOI":"10.29007\/1nbh"},{"issue":"1","key":"8_CR20","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s10817-016-9397-x","volume":"59","author":"F Frohn","year":"2017","unstructured":"Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Str\u00f6der, T.: Lower bounds for runtime complexity of term rewriting. J. Autom. Reasoning 59(1), 121\u2013163 (2017)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"8_CR21","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s10817-010-9215-9","volume":"47","author":"C Fuhs","year":"2011","unstructured":"Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dep. pairs and inductive theorem proving. JAR 47(2), 133\u2013160 (2011)","journal-title":"JAR"},{"key":"8_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58, 3\u201331 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-642-02658-4_7","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2009","unstructured":"Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 51\u201362. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_7"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/978-3-540-71070-7_32","volume-title":"Automated Reasoning","author":"N Hirokawa","year":"2008","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 364\u2013379. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_32"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-51081-8_107","volume-title":"Rewriting Techniques and Applications","author":"D Hofbauer","year":"1989","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167\u2013177. Springer, Heidelberg (1989). doi: 10.1007\/3-540-51081-8_107"},{"key":"8_CR26","unstructured":"Hoffmann, J.: Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph.D. thesis, Ludwig-Maximilians-University Munich (2011)"},{"issue":"3","key":"8_CR27","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2362389.2362393","volume":"34","author":"J Hoffmann","year":"2012","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: POPL 2017, pp. 359\u2013373 (2017)","DOI":"10.1145\/3009837.3009842"},{"key":"8_CR29","unstructured":"Hofmann, M., Moser, G.: Multivariate amortised resource analysis for term rewrite systems. In: TLCA 2015, pp. 241\u2013256 (2015)"},{"key":"8_CR30","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient completeness and related properties of term rewriting systems. Acta Informatica 24, 395\u2013415 (1987)","journal-title":"Acta Informatica"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-15984-3_291","volume-title":"EUROCAL 1985","author":"K Emmanuel","year":"1985","unstructured":"Emmanuel, K.: Completeness in data type specifications. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 348\u2013362. Springer, Heidelberg (1985). doi: 10.1007\/3-540-15984-3_291"},{"issue":"1","key":"8_CR32","doi-asserted-by":"crossref","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. Reasoning 51(1), 27\u201356 (2013)","journal-title":"J. Autom. Reasoning"},{"issue":"4\u20135","key":"8_CR33","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1017\/S147106841400057X","volume":"14","author":"A Serrano","year":"2014","unstructured":"Serrano, A., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.: Resource usage analysis of logic programs via abstract interpretation using sized types. Theory Pract. Logic Program. 14(4\u20135), 739\u2013754 (2014)","journal-title":"Theory Pract. Logic Program."},{"issue":"1","key":"8_CR34","doi-asserted-by":"crossref","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. Reasoning 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR35","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18, 528\u2013539 (1975)","journal-title":"Commun. ACM"},{"issue":"1","key":"8_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-10(1:19)2014","volume":"10","author":"H Zankl","year":"2014","unstructured":"Zankl, H., Korp, M.: Modular complexity analysis for term rewriting. Logical Meth. Comput. Sci. 10(1), 1\u201334 (2014)","journal-title":"Logical Meth. Comput. Sci."},{"issue":"1","key":"8_CR37","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symbol. Comput. 17(1), 23\u201350 (1994)","journal-title":"J. Symbol. Comput."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T03:52:38Z","timestamp":1750823558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}