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.