Öffentlicher Vortrag: Algebraische und logische Methoden zum Nachweis fehlerfreier Software

Wir möchten Sie herzlich zu folgendem Vortrag am 27.05.2021 einladen

Laura Kovacs(TU Wien)
Algebraische und logische Methoden zum Nachweis fehlerfreier Software

Abstrakt.

Unser digitales Leben ist von Software getrieben.
Es ist Software, die zum Beispiel, soziale Medien, Gesundheitswesen und den
Flugverkehr, kontrolliert.
Es ist daher alarmierend, dass Software-Infrastrukturen, die täglich genutzt
werden, fehleranfällig sind.
In diesem Vortrag werde ich zeigen, dass spezielle Softwareprogramme dazu
verwendet werden können, um zu beweisen, dass Software keine Fehler aufweist
und somit korrekt ist. Die Hauptidee dabei ist es
Computerprogramme als mathematische Objekte zu behandeln und das Fehlen von
Softwarefehlern genauso zu beweisen, wie wir Theoreme in der Mathematik beweisen.

Allerdings auch wenn alle Mathematiker der Welt ausschließlich daran arbeiten
würden Software-Eigenschaften zu beweisen, würde ihre Arbeit zu lange dauern,
wenn nicht unendlich lange. Und selbst dann könnte nur eine winzige Teilmenge
der implementierten Computerprogramme behandelt werden. Die Lösung besteht
darin, computer-unterstützte Mathematik und Logik zum Nachweis von
Softwareeigenschaften zu verwenden.
Dies ist ein wichtiger Schritt zur Reduzierung der Anzahl von Fehlern in Computerprogrammen.

 

Hier gehts zum Livestream und Videos der bisherigen Vorträge