Beweisbar sichere Software (DS2020)
Chaos Computer Club - archive feed · Marius Melzer
September 19, 202049m 44s
Audio is streamed directly from the publisher (cdn.media.ccc.de) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
Die Verifikation von Software, also das Beweisen von Eigenschaften auf Basis des Programmcodes hat in den vergangenen Jahren signifikante Fortschritte gemacht. Insbesondere die Automatisierung von Beweisen erlaubt mittlerweile eine Softwareverifikation ohne tiefgreifende Wissen in formalen Methoden.
Die ist ein Übersichtsvortrag über das Spektrum von verifizierbaren Programmiersprachen und Theorembeweisern. Es wird versucht, Idris, F*, Coq, Lean, Why3, Liquid Haskell und weitere zu kategorisieren und anhand von Beispielen Stärken und Schwächen der Ansätze aufzuzeigen.
about this event: https://datenspuren.de/2020/fahrplan/events/11315.html
Topics
DS2020113152020Technik