### Automated Sublinear Amortised Resource Analysis of Data Structures (AUTOSARD)

#### FWF Project Number: P 36623

*Wider Research Context.*
Amortised analysis is a method for the worst-case cost analysis of (probabilistic) data structures, where a single data structure operation is considered as part of a larger sequence of operations. The cost analysis of sophisticated data structures, such as self-adjusting binary search trees, has been a main objective already in the initial proposal of amortised analysis. Analysing these data structures requires sophisticated potential functions, which typically contain sublinear expressions (such as the logarithm). Apart from our pilot project, the analysis of these data structures has so far eluded automation.

*Objectives.*
We target an automated analysis of the most common data structures with good, ie. sublinear, complexity, such as balanced trees, Fibonacci heaps, randomised search trees, skip lists, skew heaps, Union-find, etc. Our goals are the verification of textbook data structures, the confirmation and improvement (on coefficients) of previously reported complexity bounds, as well as the automated analysis of realistic data structure implementations. Initially, we will only consider strict (first-order) functional programming languages. Later on, we will extend our research towards lazy evaluation in order to allow for the analysis of persistent data structures. Moreover, we will also consider probabilistic data structures.

*Methods.*
Based on the success of our pilot study, we envision the following steps for automatising amortised analysis: (i) Fix a parametrised potential function; (ii) derive a (linear) constraint system over the function parameters from the AST of the program; (iii) capture the required non-linear reasoning trough explicit background knowledge integrable into the constraint solving mechanism; and finally (iv) find values for the parameters by an (optimising) constraint solver.

#### Pilot Study

AUTOSARD is an outgrow from our pilot study on (automated) amortised cost analysis of (randomised) splay trees, pairing heaps and randomised meldable heaps.

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

Lorenz Leutgeb, Georg Moser, Florian Zuleger

Proceedings of 34rd Computer Aided Verification, pages 70--91, 2022

ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures

Lorenz Leutgeb, Georg Moser, Florian Zuleger

Proceedings of 33rd Computer Aided Verification, pp 99-122, 202

Type-Based Analysis of Logarithmic Amortised Complexity

Martin Hofmann, Lorenz Leutgeb, Georg Moser, David Obwaller, Florian Zuleger

To appear in 'Mathematical Structures in Computer Science'.

#### Duration: 4 Years

The project will start on April 1, 2023.#### Meetings

To be announced#### Members

The project is coordinated by- Georg Moser (Theoretical Computer Science; University of Innsbruck)
- Florian Zuleger (Formal Methods in Systems Engineering; Vienna University of Technology)