direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Sommersemester 2019

LV-Inhalt
Im Modul wird vermittelt, wie mit Hilfe von Werkzeugen aus dem industriellen Umfeld eine automatische Analyse für Teile einer realen Software durchgeführt werden kann.
Die Veranstaltung führt in die formale, werkzeuggestützte Verifikation von C Programmen ein. Die Programmiersprache C wird hier in ihrer vollen Mächtigkeit betrachtet, wie sie zur Programmierung von Betriebssystemkomponenten in der Praxis verwendet wird. Behandelt werden einfache Funktionsspezifikationen, Invarianten, Speichersicherheit, funktionale Korrektheit und die Korrektheit nebenläufiger Programme. Die Beispiele in der Vorlesung und die Übungsaufgaben werden mit dem von Microsoft Research entwickelten Verifikationswerkzeug VCC durchgeführt.
Die Veranstaltung stellt die technischen und wissenschaftlichen Fortschritte vor, die - ausgehend vom klassischen Hoare-Kalkül - die praktische Verifikation auch von C-Programmen in greifbare Nähe gerückt haben.
Unterrichtssprache ist englisch.
LV-Daten
Art und Form
3 LP (2 SWS Integrierte LV)
Masterstudiengang Informatik
Wahlpflichtveranstaltung
Masterstudiengang Technische Informatik
Wahlpflichtveranstaltung
LV-Nummer
2346460
Veranstalter
Santen
Zeit
Blocktermin:
23.09. - 25.09.
je 9:00 - 16:00 Uhr
Ort
TEL 1011
Anmeldung
über ISIS bis 30. April
Veranstaltungsunterlagen
ISIS

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe