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.