Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Institut für Informatik

Verteidigung Bachelorarbeit: Timon Lapawczyk

  • Wann 21.07.2016 von 10:30 bis 11:30
  • Wo 12489 Berlin, Rudower Chaussee 25, Raum 4.410
  • iCal

Herr Timon Lapawczyk verteidigt seine Bachelorarbeit zum Thema:

"Formale Verifikation von Heap-Algorithmen mit Frama-C"


 

Interessenten sind herzlich eingeladen!

 

Abstrakt:

Diese Arbeit entstand in Verbindung mit der Arbeit des Autors für die Verifikationsgruppe des Fraunhofer Instituts für Offene Kommunikationssysteme. Im Rahmen seiner Tätigkeit schrieb der Autor unter anderem am Bericht ACSL By Example mit. In ACSL By Example werden Beispiele für die formale Spezifikation von C-Funktionen mit der ANSI/ISO-C Spezifikationssprache ACSL und die deduktive Verifikation mit Frama-C und dem Plug-in WP vorgestellt. Bei der formalen Verifikation wird ein mathematischer Beweis erbracht, dass eine Funktion ihre Spezifikation erfüllt. Diese Form der Qualitätssicherung findet vor allem in sicherheitskritischen Bereichen Anwendung, in denen Fehler in der Software fatale Folgen haben können. Da die Programmiersprache C unter anderem in sicherheitskritischen eingebetteten Systemen eingesetzt wird, ist sie besonders interessant für die formale Verifikation. Die Algorithmen in dieser Arbeit stammen aus der Standard Template Library [2]. Die STL ist eine Bibliothek für die C++ Programmiersprache, aus der viele Teile in die C++ Standard Bibliothek aufgenommen wurden. Für die Verifikation mit Frama-C werden die Funktionen aus der STL in der Sprache C implementiert.
Die formale Verifikation der Heap-Algorithmen in dieser Arbeit baut auf den bisherigen Ergebnissen aus ACSL By Example auf und soll auch Teil der nächsten Version von ACSL By Example sein.