Formale Verifikation: Mehr Sicherheit für Soft- und Hardware durch Logik und Mathematik
Dr. Sebastian Ertel, Leiter der Forschungsgruppe Verified System Design Automation am Barkhausen Institut, war zu Gast im Podcast „Per Anhalter durch den Cyberraum“ der Cyberagentur. Im Gespräch mit Podcaster Marcel Roth und Dr. Dirk Pollmächer von der Cyberagentur geht es um ein Thema, das in der öffentlichen Wahrnehmung oft wenig sichtbar ist, für die Sicherheit digitaler Systeme jedoch eine zentrale Rolle spielt: Formale Verifikation.
Formale Verifikation nutzt mathematische Methoden, um Software und Systeme systematisch zu überprüfen. Ziel ist es, nachzuweisen, dass Programme korrekt funktionieren und keine unerwarteten oder unsicheren Zustände annehmen können. Gerade bei komplexen und sicherheitskritischen Anwendungen gewinnt dieser Ansatz zunehmend an Bedeutung.
Im Podcast erläutert Sebastian Ertel, warum formale Methoden helfen können, Vertrauen in digitale Technologien zu stärken und weshalb sie auch im Kontext von Künstlicher Intelligenz eine wichtige Rolle spielen. Gleichzeitig wird deutlich, dass hinter Informatik und Mathematik oft grundlegende Fragen stehen, die weit über technische Details hinausgehen.
Hier finden sie die vollständige Folge „Hard- und Software sicher machen - mit Logik und Mathe“.