Navigation Zur Modulseite
Anzeigesprache

Applied Verification of C-Programs
Verifikation von C-Programmen in der Praxis

3

Deutsch

#40278 / #2

SS 2017 - WS 2021/22

Fakultät IV

TEL 12-4

Institut für Softwaretechnik und Theoretische Informatik

34351800 FG Software and Embedded Systems Engineering (SESE)

Glesner, Sabine

Berg, Nils Erik

lehre@sese.tu-berlin.de

POS-Nummer PORD-Nummer Modultitel
2346460 37413 Applied Verification of C-Programs

Lernergebnisse

In diesem Modul werden den Teilnehmerinnen und Teilnehmern Wissen über die formale Verifikation von Programmen und Fähigkeiten und Erfahrungen im praktischen Umgang mit Werkzeugen für die automatische Softwareanalyse vermittelt.

Lehrinhalte

Dieses Modul wird von Dr.-Ing. habil. Thomas Santen (thomas.santen@outlook.com) veranstaltet. 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 der letzten 12 Jahre vor, die - ausgehend vom klassischen Hoare-Kalkül - die praktische Verifikation auch von C-Programmen in greifbare Nähe gerückt haben.

Modulbestandteile

Pflichtgruppe:

Die folgenden Veranstaltungen sind für das Modul obligatorisch:

Lehrveranstaltungen Art Nummer Turnus Sprache SWS VZ
Verifikation von C-Programmen in der Praxis IV 0434 L 196 SS Englisch 2

Arbeitsaufwand und Leistungspunkte

Verifikation von C-Programmen in der Praxis (IV):

Aufwandbeschreibung Multiplikator Stunden Gesamt
2 Verifikations Aufgaben 2.0 10.0h 20.0h
Multiple Choice 1.0 2.0h 2.0h
Präsenzzeit 3.0 8.0h 24.0h
Vor-/Nachbereitung 1.0 44.0h 44.0h
90.0h(~3 LP)
Der Aufwand des Moduls summiert sich zu 90.0 Stunden. Damit umfasst das Modul 3 Leistungspunkte.

Beschreibung der Lehr- und Lernformen

Die Veranstaltung wird als mehrtägige Blockveranstaltung durchgeführt. Einführende Vorlesungen zur Theorie der Verifikation von C-Programmen werden mit praktischen Übungen abwechseln, die mit dem bei Microsoft Research entwickelten Verifikationswerkzeug VCC durchgeführt werden. Zum Abschluss wird eine Verifikationsaufgabe gestellt, die eigenständig mit VCC zu lösen ist. Zur Bearbeitung der Aufgaben ist ein Rechner unter Windows 7, Vista oder XP notwendig, auf dem Visual Studio 2012 und VCC (vcc.codeplex.com) installiert werden. Hardware und Betriebssystem können nicht zur Verfügung gestellt werden. Visual Studio ist unter der Dreamspark (www.eecs.tu-berlin.de/irb/v-menu/dienstleistungen/dreamspark/) für Studierende frei verfügbar.

Voraussetzungen für die Teilnahme / Prüfung

Wünschenswerte Voraussetzungen für die Teilnahme an den Lehrveranstaltungen:

Kenntnisse in der Programmiersprache C, Prädikatenlogik erster Stufe und Hoare-Kalkül sind hilfreich.

Verpflichtende Voraussetzungen für die Modulprüfungsanmeldung:

Keine Angabe

Abschluss des Moduls

Benotung

benotet

Prüfungsform

Portfolioprüfung

Art der Portfolioprüfung

100 Punkte insgesamt

Sprache

Deutsch

Prüfungselemente

Name Punkte Kategorie Dauer/Umfang
(Ergebnisprüfung) 2 Verifikationsaufgaben mit je 40 Punkten 80 praktisch 2*10h=20h
(Punktuelle Leistungsabfrage) Multiple Choice Aufgabe 20 schriftlich 30-60min

Notenschlüssel

1.01.31.72.02.32.73.03.33.74.0
95.090.085.080.075.070.065.060.055.050.0

Prüfungsbeschreibung (Abschluss des Moduls)

Keine Angabe

Dauer des Moduls

Für Belegung und Abschluss des Moduls ist folgende Semesteranzahl veranschlagt:
1 Semester.

Dieses Modul kann in folgenden Semestern begonnen werden:
Sommersemester.

Maximale teilnehmende Personen

Dieses Modul ist nicht auf eine Anzahl Studierender begrenzt.

Anmeldeformalitäten

Anmeldung zu Beginn des jeweiligen Semesters (Aushang / Ankündigung auf der Internetseite http://www.sese.tu-berlin.de/ beachten).

Literaturhinweise, Skripte

Skript in Papierform

Verfügbarkeit:  nicht verfügbar

Skript in elektronischer Form

Verfügbarkeit:  nicht verfügbar

Literatur

Empfohlene Literatur
Keine empfohlene Literatur angegeben.

Zugeordnete Studiengänge

Diese Modulversion wird in folgenden Studiengängen verwendet:

Diese Modulversion wird auf folgenden Modullisten verwendet (alte Studiengangsabbildung):

Sonstiges

Dieses Modul wird von Dr.-Ing. habil. Thomas Santen (thomas.santen@outlook.com) durchgeführt.