2026-07-23T21:03:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5206 2024-03-06T10:36:04Z ddc:004 open_access

Inferring Lower Bounds for Runtime Complexity Frohn, Florian Giesl, Jürgen Hensel, Jera Aschermann, Cornelius Ströder, Thomas Term Rewriting Runtime Complexity Lower Bounds Induction We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in the tool AProVE and evaluated it by extensive experiments. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Florian Frohn and Jürgen Giesl and Jera Hensel and Cornelius Aschermann and Thomas Ströder 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.334 urn:nbn:de:0030-drops-52068 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.334 eng https://creativecommons.org/licenses/by/3.0/legalcode