Korrektheit von Programmen beweisen mit Coq

17:00 bis 18:00 in Raum V2

Peter Hrenka

“Jede nicht-triviale Software hat Fehler!” - Wirklich? Es gibt mittlerweile (mindestens) einen C-Compiler, ein Dateisystem und ein Betriebsystem deren Implementierung von Beweisassistenzsystemen gegen deren Spezifikation verifiziert wurden. Der Vortrag soll einen kleinen Einblick liefern wie man mit dem Beweisassistenzsystem Coq mathematische Sätze beweisen und Software implementieren und verifizieren kann.

Vorwissen

Programmiererfahrung