Prof. Dr. Bernhard Beckert ist Leiter der Arbeitsgruppe Anwendungsorientierte Formale Verifikation am KIT. Seine Forschungsinteressen umfassen den Einsatz formaler Methoden in der Softwareentwicklung, sowie automatisches Schließen und nichtklassische Logiken. Das Ziel ist es, mittels formaler Methoden die Korrektheit und Sicherheit von Systemen zu erhöhen.

Die aktuellen Forschungsschwerpunkte beinhalten die Spezifikation und den formalen Nachweis von Eigenschaften objektorientierter Programme. Dazu gehören sowohl die korrekte Funktionalität von Programmen, als auch Eigenschaften des Informationsflusses in Programmen als ein sicherheitsrelevanter Aspekt von Software-Systemen.

Anwendungsorientierte Formale Verifikation

Das Forschungsgebiet der Arbeitsgruppe sind Formale Methoden und deren Anwendung in der Softwareentwicklung. Die Arbeiten befassen sich dabei mit der Beschreibung von Programmeigenschaften (Spezifikation), sowie deren formalen Nachweis (der deduktiven Verifikation), jeweils auf der Ebene des Programm-Quelltexts.

Neben theoretischer Grundlagenforschung, zum Beispiel im Bereich der Semantik von Programmiersprachen und bei der Entwicklung geeigneter Spezifikationssprachen und Deduktionskalküle, spielt die Entwicklung praxistauglicher formaler Methoden zur Integration mit konventionellen Methoden der Softwareentwicklung eine wichtige Rolle.

Die aktuellen Forschungsschwerpunkte der Arbeitsgruppe liegen bei der Spezifikation und deduktiven Verifikation von Eigenschaften objektorientierter Programme. Insbesondere der Nachweis von Informationsflusseigenschaften auf Programmebene zur Gewährleistung von Sicherheitseigenschaften eines Programms ist ein aktueller Schwerpunkt der Arbeiten.