Korrektheit sollte eigentlich eine selbstverständliche Anforderung an Software sein, schafft es dennoch selten in die offizielle Design-Dokumentation. Aber: Manche Software *muss* korrekt sein - solche, die kritische Hardware steuert, sensible Informationen schützt oder umsatzkritische Berechnungen anstellt. Leider sind Entwicklungsprozesse oft fehleranfällig, und bekanntermaßen können alle Tests der Welt nur die Anwesenheit von Fehlern zeigen, nicht aber deren Abwesenheit.

Um dafür Gewissheit zu bekommen, brauchen wir Beweise - mathematische, formale Beweise. Inzwischen gibt es aber ein großes Arsenal von Techniken und Werkzeugen, die dabei helfen, Korrektheitsbeweise zu erstellen und zu überprüfen. Der Vortrag gibt einen Überblick über Technik und Technologie.

Mehr Inhalte dieser Speaker? Schaut doch mal bei sigs.de vorbei: https://www.sigs.de/autor/michael.sperber, https://www.sigs.de/autor/lars.hupel