VERIFIKATION VON MEHRSTRÄNGIGEN PROGRAMMEN UND PARAMETRIERTE VERIFKATION.
Viele moderne IT-Systeme sind über verschiedene physische Standorte verteilt und es wird erwartet, dass sie in Parametern wie der Anzahl der gleichzeitig laufenden Threads oder der Anzahl der Benutzer:innen skalierbar sind. Solche Systeme werden routinemäßig eingesetzt, um mit sensiblen Informationen umzugehen oder sicherheitskritische Prozesse zu steuern, zum Beispiel im Cloud Computing, in industriellen Steuerungssystemen oder drahtlosen Sensornetzen. Der Aufbau verteilter Systeme ist jedoch sehr komplex und fehleranfällig, da alle möglichen Interaktionen zwischen Systemkomponenten, einschließlich Hardware- oder Netzwerkausfällen, sowie böswillige Gegner:innen berücksichtigt werden müssen. Wir untersuchen das grundlegende Problem, Korrektheitsgarantien für verteilte Systeme mit einer großen Anzahl von Komponenten zu erhalten.
Verifikation mehrsträngiger Programme. Um Verifikationsmethoden auf große Parameterwerte, wie z.B. die Anzahl der Stränge in Multithread-Programmen, zu skalieren, untersuchen wir die grundlegenden Abhängigkeiten zwischen den einzelnen Strängen eines Programms in Bezug auf ein bestimmtes Ziel, wie z.B. die erfolgreiche Beendigung. Auf der Grundlage eines tiefen Verständnisses ihrer Wechselwirkungen entwickeln wir neuartige Verifikationsparadigmen, die nicht direkt von der Anzahl der Programmstränge abhängen und daher auf sehr große Werte dieses Parameters skalieren.
Parametrisierte Verifizierung. Wir erforschen Klassen von Systemen, für die unabhängig von der Anzahl der Komponenten oder Teilnehmer:innen Korrektheitsgarantien gegeben werden können. Wir untersuchen systematisch die Beziehungen zwischen verschiedenen Systemmodellen, um grundlegende Erkenntnisse darüber zu gewinnen, welche Klassen von Programmen sie erfassen und welche ihrer Eigenschaften automatisch bestimmt werden können. Wir entwickeln anwendungsspezifische Abstraktionen von Systemen beliebiger Grösse, auf denen wir Algorithmen aufbauen, die unabhängig von der Grösse des Systems Sicherheitsgarantien geben können.
Verteilte und parametrisierte Synthese. Bei komplexen Interaktionen zwischen Komponenten sowie bei unvorhergesehenen Ausfällen und Gegner:innen sind die gewünschten Eigenschaften verteilter Systeme in der Regel viel einfacher zu spezifizieren als zu implementieren. Daher sind sie ein vorrangiges Ziel für formale Synthesetechniken, die eine Beschreibung der gewünschten Eigenschaften in einer formalen Spezifikationssprache automatisch in ein konstruktionsgerechtes, verteiltes System transformieren. Wir untersuchen Grundlagen und Methoden der formalen Synthese, einschließlich Voraussetzungen für ihre Anwendung sowie neue Syntheseparadigmen, die qualitativ hochwertige Implementierungen erzeugen.
