PoP Seminar Talk

Automated Expected Cost Analysis of Splaying et al.

Georg Moser, Professor for Computer Science, University of Innsbruck
Thursday, 08 June, 2023; 3:00pm
GHC 4405
Host: Jan Hoffmann


In this talk, I present recent work on fully-automated (expected) amortised cost analysis of self-adjusting data structures, like splay trees or splay heaps, as well as probabilistic data structures like randomised splay trees or splay heaps and randomised meldable heaps. Prior to our work, these data structures have only (semi-)manually been analysed in the literature.

Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models.

With our prototype implementation, we have been able automatically infer bounds on the (expected) amortised cost, which could previously only be obtained by sophisticated pen-and-paper proofs. In particular, we verify that the amortised costs of randomised variants of self-adjusting data structures improve upon their non-randomised variants.

This is joint work with Lorenz Leutgeb and Florian Zuleger.


Georg Moser is a Full Professor of Theoretical Computer Science at the University of Innsbruck since February 2020. He studied Computer Science and Logic at the Vienna University of Technology and the University of Leeds, respectively. Prior to his appointment to full professor, he has been an associate professor at the University of Innsbruck, heading a reserach group on computation with bounded resources. His research interests centre around logic and program analysis. For the latter, a recent focus of his work is on probabilistic programming and Quantum computation. He has lead a number of national and international research consortia. He has acted as steering committee chair and member of international conference series and similar research consortia and continues to do so. Moreover, he has been chair of the IFIP Working Group 1.6. His expertise is frequently sought as a program committee member of most prominent conferences such as FSCD, LICS, etc. Further, he has frequently provided editorial services.