Theoretical Computer Science

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 Further (prospective) project members will be announced here, timely.