Formale Methoden werden genutzt, um von realen Systemen zu abstrahieren und sich dabei auf bestimmte Aspekte solcher Systeme zu fokussieren. Solch ein Aspekt kann zum Beispiel die Kommunikationsstruktur eines Systems, deren Grad an Privatheit oder Kryptographische Eigenschaften umfassen. Die Komplexität der Interaktionen in realen Systemen und die große Anzahl erreichbarer Zustände erschwert die Analyse solcher Systeme und macht sie oft ineffizient oder unpraktikabel. Der Forschungsbereich, der sich mit diesen Problemen beschäftigt, wird oft Nebenläufigkeitstheorie (Concurrency Theory) genannt.
Es gibt viele verschiedene Modellierungssprachen im Bereich Concurrency. Wir arebeiten oft mit Prozesskalkülen und seit neuerem auch mit Multiparty Session Types, weil diese Sprachen relativ nahe an Programmiersprachen verortet sind. Aber wir sind auch an allen anderen Modellierungssprachen wie z.B. Petrinetzen oder Event Structures interessiert. Die beiden letzteren Sprachen sind besonders nützlich für die Analyse von Kontrollflüssen und kausalen Abhängigkeiten, aber sie modellieren die Interaktion und Verteilung in Systemen nicht so direkt.
Ein großer Teil unserer Forschung beschäftigt sich mit der Analyse, dem Vergleich und Erweiterungen von Concurrency Formalismen. Wir untersuchen welche Modellierungssprachen sich für welche Probleme eignen und wie Modellierungssprachen für neue Anwendungsgebiete erweitert werden können. Diese Forschung hilft bei der Wahl passender Modellierungssprachen und hilft so bei der Analyse realer Systeme.
Um unsere Forschung formal zu unterstützen und um deren Korrektheit zu garantieren, nutzen wir manchmal den interaktiven Theorembeweiser Isabelle/HOL.
