This paper presents a major-step forward towards fully automated amortised complexity analysis of functional data structures. We extend our type-inference based static analyisis tool ATLAS into a flexible and more expressive analysis framework. Instead of relying on a single, fixed analysis strategy, the system supports a wide range of potential functions.
These advances allowed us to complete the previously outstanding analysis of skew heaps and analyize leftist heaps in a fully automated amortised setting.
The extended system also introduces path senstitve reasoning and support for data structure invariants, which are crucial to leftist heaps and that we expect will enable the automated analysis of a much broader class of data structures.
This is joint work with and Berry Schoenmakers (TU Eindhoven) and Florian Zuleger (TU Wien).