Computer Science Graduate Seminar: Automated Complexity Analysis of Rewrite Systems
Tuesday, December 11, 2018, 4:15pm
Location: E3 building, Seminar room 9222, Ahornstr. 55
Speaker: Florian Frohn, M.Sc., Lehr- und Forschungsgebiet Informatik 2
Besides functional correctness, one of the most important prerequisites for the success of software is efficiency: The desired results need to be computed not only correctly, but also in time. Thus, analyzing the runtime complexity of software is indispensable in practice. Unfortunately, analyzing the complexity of large programs manually is infeasible. Hence, automated complexity analysis techniques are needed. In this way, performance pitfalls can be highlighted automatically like other bugs which can nowadays be found by compilers or static analyzers.
However, statically analyzing the complexity of real-world programs poses several problems. For example, most programming languages lack formal semantics. Moreover, different programming languages offer different features, so static analyses for one language do not necessarily apply to others. A common solution for these problems is to transform programs into low-level formalisms like integer or term rewrite systems that can be analyzed without worrying about language-specific peculiarities.
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.
The computer science lecturers invite interested people to join.