Software Verification

Software schreiben ist schwierig. Ein Tool, das immer wieder kurze Zeit auf kommt, um danach wieder zu verschwinden, ist die (automatische, statische) Verifikation von Software. Ziel ist, mit einem Algorithmus fest zu stellen, ob ein Programm “korrekt” funktioniert. In diesem Vortrag geht es hauptsächlich darum klar zu machen, warum Verifikation sich nicht wirklich durchgesetzt hat, was denn “korrekt” heißen soll, wofür man Verifikation sonst noch einsetzen kann, und letztlich was man aus das ganze lernen kann ohne es anwenden zu müssen.