Automated complexity analysis of rewrite systems

Besides functional correctness, one of the most important prerequisites for the success of a piece 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. On the other hand, 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 term or integer rewrite systems that can be analyzed without worrying about language-specific peculiarities. Unfortunately, state-of-the-art complexity analysis techniques for rewrite systems have several limitations. Firstly, most of them are restricted to the inference of upper bounds on the worst-case complexity. Moreover, existing complexity analyzers only reach their full potential if an eager evaluation strategy is fixed, which is sometimes undesired in practice. Finally, many techniques for integer rewriting just support tail recursion. This thesis partially overcomes these limitations. To this end, the first techniques for the inference of lower bounds on the worst-case complexity are introduced. One important use case of such lower bounds is to witness denial-of-service vulnerabilities (whose absence can be proven via upper bounds), which arise if the runtime of a program exceeds expectations. Regarding upper bounds, this thesis shows how complexity analysis techniques for term rewriting which require an eager evaluation strategy can also be used without assuming eager evaluation. Similarly, it shows how complexity analysis techniques for integer rewriting which are restricted to tail recursion can also be used to analyze non-tail-recursive systems. Consequently, complexity-preserving transformations to rewrite systems can now be used for more applications - like the detection of denial-of-service vulnerabilities - and richer classes of programs. This is true for both programs operating on integers as well as programs operating on tree-shaped data, which can naturally be transformed to integer and term rewrite systems, respectively. Hence, this thesis covers a large subset of the features provided by real-world programming languages. The presented techniques were implemented in the tools AProVE and LoAT, which can analyze the complexity of rewrite systems fully automatically. Extensive experiments demonstrate the feasibility of the presented techniques in practice