Forschung

Unsere Forschung kann grob unter im Bereich der Formalen Methoden zur Konstruktion und Analyse von Systemen eingeordnet werden.

Interessensschwerpunkte sind: Werkzeuge zum Compilerbau, statische Analyse durch Abstrakte Interpretation und Model Checking, effiziente generische Fixpunktalgorythmen, ausdrucksstarke Domänen für numerische Invariants, Analyse nebenläufiger Systeme, Präzision von Analysen, Analysen von sicherheitskritischen C Programmen, Datenflußanalyse, Analyse kryptographischer Protokolle, Baumautomaten und Hornklauseln, Baumautomaten und XML Verarbeitung, Äquivalenzprobleme für Baumautomaten.

Wir interessieren uns ausserdem für innovative Technische Systeme zum für Unterricht und zur Visualisierung von Systemabläufen.

Die meisten unserer Ideen sind in Prototypen implementiert, wie zum Beispiel CUP (ein Frontendgenerator für Java), Goblint (ein Analysator für multithreaded C) oder ttt (ein System zur Vorlesungsaufzeichnung).

Unsere Forschungsgruppe hat einen Beitrag zum Bau von Quantencomputern im Munich Quantum Valley geleistet. Schauen Sie bei Yanbin Chen für weiteres Interesse. Derzeit konzentrieren wir uns hauptsächlich auf statische Analysen und Optimierungen für dynamische Quantenschaltungen.