Self-adjusting data structures such as splay trees, skew heaps, pairing heaps, etc. are popular because they are simple to implement and have been demonstrated to show good performance in practice. The formal analysis of their computational complexity, however, is intricate and requires the concept of amortized complexity, which is typically only covered in courses on efficient data structures. In this master thesis topic, we aim at automating previous pen-and-proofs of amortized complexity. The goal is to improve the automated complexity analysis of [1] and [2], which is currently only able to handle splay trees, splay heaps and pairing heaps. The first goal is to extend the analysis to skew heaps and to provide an improved analysis of pairing heaps. A possible further target is the analysis of Fibnoacci heaps.

• Lorenz Leutgeb, Georg Moser, Florian Zuleger: ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. CAV (2) 2021: 99-122
• Martin Hofmann, Lorenz Leutgeb, David Obwaller, Georg Moser, Florian Zuleger: Type-based analysis of logarithmic amortised complexity. Mathematical Structures in Computer Science (2021): 1-33. doi:10.1017/S0960129521000232

In contrast to the wealth of literature on the (automated) resource analysis of strict language, like OCaml, the resource analysis of non-strict languages, like Haskell, has received scarce attention. One notable exception is Okasaki, who adapted the banker's method of amortised cost analysis to the debit method, in order to correctly analyse the amortised costs of lazy data structures. In this master thesis project, we aim to study and formalse his approach. In particular we aim to adapt recent work on the fully automated amortised analysis of self-adjusting data structures such as splay trees, splay heaps, pairing heaps [3,4] to lazy evaluation. The first goal is a rigorous formalisation of the Okasaki's debit method for the amortised analysis of non-strict functional programs, second the implementation of this formal methodology is envisioned as well as the application of this prototype implementation to popular lazy data structures, like lazy skew heaps. A possible further target could be lazy pairing heaps.

• C. Okasaki, Purely functional data structures, Cambridge University Press, 1999

In recent years interest and techniques in resource analysis of probabilistic programs have significantly increased. In the project, we study a recent approach for the automated complexity analysis of probablisitic term rewrite systems (PTRS) due to Avanzini et al., with the goal of implementing the methods in TcT. A further goal is the (potential) improvement of the theory and methods.

• On Probabilistic Term Rewriting
  Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
  Proc. 14th International Symposium on Functional and Logic Programming, LNCS 10818, pp. 132 – 148, 2018
• TcT: Tyrolean Complexity Tool
  Martin Avanzini, Georg Moser, Michael Schaper
  Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 9636, pp. 407 – 423, 2016

First-order theorem provers have developed rapidly over the last decades. Nowadays these provers are employed in the formal analysis of software, systems, protocols, formal approaches to AI planning, decision procedures, etc. It is a well-known challenge to automate first-order reasoning with equality. One of the best known method here is the superposition calculus, which has been implemented successfully in theorem provers like SPASS. Furthermore, recently instantiation-based methods have been studied in the context of automated reasoning with equality. As a first step to the development of our own instantiation-based theorem prover for equality, we develop in this project a superposition based theorem prover.

We can induce polynomial upper bounds on the derivational complexity of a term rewrite system if we find a compatible matrix interpretation whose maximum matrix has spectral radius at most one. Starting from root counting algorithms of the mathematical literature, we investigate the performance of several constraints which ensure this condition is met.