Die Teilnahme an mindestens einem Masterseminar in der TCS-Gruppe ist für alle Masterarbeiten verpflichtend.
Probabilistic Term Rewriting
In den letzten Jahren haben das Interesse und die Techniken zur Ressourcenanalyse probabilistischer Programme erheblich zugenommen. Im Projekt untersuchen wir einen aktuellen Ansatz zur automatisierten Komplexitätsanalyse probablisitischer Term-Rewrite-Systeme (PTRS) von Avanzini et al. mit dem Ziel, die Methoden in TcT zu implementieren. Ein weiteres Ziel ist die (potenzielle) Verbesserung der Theorie und Methoden.
- On Probabilistic Term Rewriting
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
Proc. 14. Internationales Symposium für funktionale und logische Programmierung, LNCS 10818, S. 132–148, 2018 - TcT: Tyrolean Complexity Tool
Martin Avanzini, Georg Moser, Michael Schaper
Proc. 22. Internationale Konferenz über Tools und Algorithmen für die Konstruktion und Analyse von Systemen, LNCS 9636, S. 407–423, 2016
Komplexitätsanalyse von Lazy Programmen
Im Gegensatz zu der Fülle an Literatur über die (automatisierte) Ressourcenanalyse von strikten Sprachen wie OCaml wurde der Ressourcenanalyse von nicht-strikten Sprachen wie Haskell kaum Aufmerksamkeit geschenkt. Eine bemerkenswerte Ausnahme ist Okasaki, der die Bankier-Methode der Amortisationskostenanalyse an die Debit-Methode angepasst hat, um die Amortisationskosten von lazy Datenstrukturen korrekt zu analysieren. In dieser Masterarbeit wollen wir seinen Ansatz untersuchen und formalisieren. Insbesondere wollen wir die jüngsten Arbeiten zur vollautomatischen Amortisationsanalyse von selbstanpassenden Datenstrukturen wie Splay Trees, Splay Heaps und Pairing Heaps an die lazy evaluation anpassen. Das erste Ziel ist eine rigorose Formalisierung der Okasaki's Debit-Methode für die amortisierte Analyse von nicht-strikten funktionalen Programmen, zweitens ist die Implementierung dieser formalen Methodik vorgesehen sowie die Anwendung dieser prototypischen Implementierung auf populäre faule Datenstrukturen, wie z.B. Lazy Skew Heaps. Ein mögliches weiteres Ziel könnten Lazy Pairing Heaps sein.
- Purely functional data structures Chris Okasaki, Cambridge University Press 1999, ISBN 978-0-521-66350-2, pp. I-X, 1-220
Multivariate Amortisierte Ressourcenanalyse
In jüngster Zeit hat die Amortisationsanalyse in der Ressourcenanalyse großes Interesse gefunden. In diesem Masterprojekt werden wir die verschiedenen Ansätze untersuchen und insbesondere aktuelle Ergebnisse zur multivariaten amortisierten Analyse von Termumschreibsystemen umsetzen. Dies wird unter anderem die automatische Synthese von Baumautomaten beinhalten, die zur Definition des Potentials von Werten über beliebige benutzerdefinierte Datentypen eingesetzt werden.
- Amortised Resource Analysis and Typed Polynomial Interpretations Martin Hofmann, Georg Moser, RTA-TLCA 2015
Portierung von ATLAS zu Haskell
ATLAS (Automated Amortised Complexity Analysis of Self-Adjusting Data Structures) bietet eine vollautomatische Analyse der erwarteten amortisierten Kosten von selbstanpassenden Datenstrukturen, d.h. von randomisierten Splay Trees, randomisierten Splay Heaps, randomisierten meldable Heaps und anderen anspruchsvollen Datenstrukturen (nicht notwendigerweise randomisiert), die bisher in der Literatur nur (halb-)manuell analysiert wurden. Der aktuelle Prototyp ist in Java implementiert und soll nach Haskell portiert werden. Wenn möglich, sollte diese Re-Implementierung auch die Klasse der betrachteten Ressourcenfunktionen erweitern.
- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures Lorenz Leutgeb, Georg Moser, Florian Zuleger, CAV 2021
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures Lorenz Leutgeb, Georg Moser, Florian Zuleger, CAV 2022
Keine Einträge.
Real Root Counting und Ableitungskomplexität von Term-Rewrite-Systemen
Wir können polynomiale Obergrenzen für die Ableitungskomplexität eines Term-Rewrite-Systems induzieren, wenn wir eine kompatible Matrixinterpretation finden, deren maximale Matrix einen Spektralradius von höchstens eins hat. Ausgehend von Root Counting Algorithmus der mathematischen Literatur untersuchen wir die Leistung verschiedener Einschränkungen, die sicherstellen, dass diese Bedingung erfüllt ist.
Student_in
Philipp Wirtenberger
Betreuer_in
Georg Moser