Forschungsgruppe
Finkbeiner
Reaktive Systeme
Wir entwickeln Methoden für den Entwurf von Systemen, die nachweislich sicher sind. Unsere Techniken sind in formalen Methoden und Mathematik verwurzelt und decken den gesamten Softwareentwicklungsprozess ab, von den Anforderungen bis zum Einsatz. Wir entwerfen ausdrucksstarke Spezifikationssprachen (temporale Logiken, Hyperproperties), Algorithmen für die automatische Programmsynthese und -reparatur (Controller-Synthese, ausgangssensitive Synthese) sowie Werkzeuge für die statische Verifikation (MCHyper) und die Laufzeitüberwachung und -durchsetzung (RTLola). Unsere Forschung hat unmittelbare Auswirkungen auf Bereiche wie verteilte, mobile und autonome Systeme und schafft Grundlagen, die uns helfen, die digitalen Systeme zu verstehen, die die Gesellschaft von morgen bestimmen.
