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 announcedMembers
The project is coordinated by- Georg Moser (Theoretical Computer Science; University of Innsbruck)
- Florian Zuleger (Formal Methods in Systems Engineering; Vienna University of Technology)