Forschungsprojekte
VASSAL
VASSAL (Verification and Analysis for Safety and Security of Applications in Life) ist ein von der Europäischen Union im Rahmen von Horizon Europe gefördertes Projekt. Es baut ein virtuelles Forschungszentrum für die Grundlagen automatisierter Verifikation, Analyse und modellbasierter Entwicklung sicherer Software auf, von Logik und Automaten bis zur Analyse auf Quellcodeebene, und untersucht zugleich die ökonomischen Auswirkungen dieser Technologien für kleine und mittlere Unternehmen. Kooperationspartner sind die Technische Universität Brno, die Masaryk-Universität Brno und CEA Paris-Saclay.
AUTOSARD
AUTOSARD (Automated Sublinear Amortised Resource Analysis of Data Structures) ist ein FWF-Projekt (P 36623), das wir gemeinsam mit Georg Moser (Universität Innsbruck) durchführen. Datenstrukturen mit sublinearer Komplexität, etwa selbstanpassende Suchbäume, Fibonacci-Heaps oder Skip-Listen, erfordern für ihre amortisierte Kostenanalyse Potentialfunktionen mit sublinearen Anteilen wie dem Logarithmus, was sich einer Automatisierung bisher weitgehend entzogen hat. Wir automatisieren diese Analyse, indem wir aus dem Syntaxbaum des Programms ein Constraint-System über den Parametern einer fixierten Potentialfunktion ableiten und dieses mit einem optimierenden Löser bestimmen. Ausgehend von funktionalen Programmen erweitern wir den Ansatz auf persistente und probabilistische Datenstrukturen.