Beweisbar sichere Software

Entdecke in diesem 50-minütigen Vortrag von der media.ccc.de-Konferenz die Fortschritte in der Softwareverifikation und beweisbaren Sicherheit. Tauche ein in die Welt der verifizierbaren Programmiersprachen und Theorembeweiser, während Marius Melzer einen umfassenden Überblick über Sprachen wie Idris, F*, Coq, Lean, Why3 und Liquid Haskell gibt. Lerne anhand von praktischen Beispielen die Stärken und Schwächen verschiedener Ansätze kennen, von der Einführung in die Grundlagen bis hin zu komplexen Beweisführungen. Verstehe, wie die Automatisierung von Beweisen die Softwareverifikation auch ohne tiefgreifendes Wissen in formalen Methoden ermöglicht und erfahre mehr über bedeutende Projekte wie Deep Spec und Project Everest. Erkunde die Verwandtschaft zwischen Beweisen und Programmen und lerne, wie übliche Spezifikationen umgesetzt werden können, einschließlich der Behandlung von Index-out-of-bounds-Fehlern und der Durchführung von Fallunterscheidungen.

Einleitung
Wieso das ganze?
Leuchtturmprojekte: Deep Spec
Leuchtturmprojekte: Project Everest
Beweise und Programme sind verwandt!
Sprachen und Systeme
Übliche Spezifikationen
Index out of bounds!
Beispiel: getNth
Beispiel in Haskell
Fallunterscheidungen
Beweise als Typen
Beispiel in Coq
Unmöglichkeitsbeweis
Beweis durch Fallunterscheidung
Beispiel in Liquid Haskell
Weitere einfache Beispiele