Florian Frohn

"Automated Complexity Analysis of Rewrite Systems"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

Many approaches to analyze the complexity of programs automatically are based on transformations into integer or term rewrite systems. However, state-of-the-art tools that analyze the worst-case complexity of rewrite systems are restricted to the inference of upper bounds. In this talk, the first techniques for the inference of lower bounds on the worst-case complexity of integer and term rewrite systems are introduced. While upper bounds can prove the absence of performance-critical bugs, lower bounds can be used to find them.
For term rewriting, the power of the presented technique gives rise to the question whether the existence of a non-constant lower bound is decidable. Thus, the corresponding decidability results are also discussed in this talk.
Finally, to see the practical value of complexity analysis techniques for rewrite systems, we will have a glimpse at the transformation from Java programs to integer rewrite systems that is implemented in the tool AProVE.

Bio: Florian Frohn is a research assistant at Lehr- und Forschungsgebiet Informatik 2 at RWTH Aachen. In December 2018, he successfully defended his PhD thesis.