Diese Arbeit stellt einen bedeutenden Fortschritt auf dem Weg zur vollständig automatisierten amortisierten Komplexitätsanalyse funktionaler Datenstrukturen dar. Wir erweitern unser auf Typinferenz basierendes statisches Analysewerkzeug ATLAS zu einem flexiblen und ausdrucksstärkeren Analyseframework. Anstatt sich auf eine einzelne, fest vorgegebene Analysestrategie zu stützen, unterstützt das System eine breite Klasse von Potentialfunktionen.
Diese Fortschritte ermöglichen es uns, die bislang offene Analyse von Skew-Heaps abzuschließen und Leftist-Heaps erstmals vollständig automatisiert im amortisierten Setting zu analysieren.
Das erweiterte System führt zudem pfadsensitive Analyse sowie die Unterstützung von Datenstrukturinvarianten ein – beides entscheidend für die Behandlung von Leftist-Heaps und, wie wir erwarten, grundlegend für die automatisierte Analyse einer deutlich größeren Klasse von Datenstrukturen.
Diese Arbeit entstand in Zusammenarbeit mit Berry Schoenmakers (TU Eindhoven) und Florian Zuleger (TU Wien).