Wir beschäftigen uns mit formalen, mathematisch präzisen Methoden zur Beschreibung und Analyse von Systemen der Informatik. Die entwickelten Methoden setzen wir in Werkzeugen um und erproben sie an realen Fallstudien. Neben allgemeinen Verifikationsverfahren fokussieren wir uns in der Anwendung momentan auf (a) die Verifikation von parallelen Programmen, insbesondere parallelen Datenstrukturen und Software Transactional Memory Algorithmen, (b) die Taint-Analyse von Android Apps und (c) die Analyse von „gelernter“ Software. Genauere Informationen finden sich auf unseren Forschungsseiten.