+**********************************************************************
*
*
*                          Einladung
*
*
*
*                     Informatik-Oberseminar
*
*
*
+**********************************************************************

Zeit:  Dienstag, 11. Dezember 2018, 16:15 Uhr
Ort:   Gebäude E3, Seminarraum 9222, Ahornstr. 55

Referent: Florian Frohn, M.Sc.
          Lehr- und Forschungsgebiet Informatik 2

Thema: Automated Complexity Analysis of Rewrite Systems

Abstract:

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.


Es laden ein: Die Dozenten der Informatik