Beweisbar sichere Software (DS2020)

49:44
 
Teilen
 

Manage episode 272456006 series 48696
Von CCC media team entdeckt von Player FM und unserer Community - Das Urheberrecht hat der Herausgeber, nicht Player FM, und die Audiodaten werden direkt von ihren Servern gestreamt. Tippe auf Abonnieren um Updates in Player FM zu verfolgen oder füge die URL in andere Podcast Apps ein.
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

9749 Episoden