Anzeigesprache
Zur Modulseite PDF generieren

#40278 / #2

SS 2017 - WiSe 2021/22

Deutsch

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

3

Glesner, Sabine

benotet

Portfolioprüfung

Zugehörigkeit


Fakultät IV

Institut für Softwaretechnik und Theoretische Informatik

34351800 FG Software and Embedded Systems Engineering (SESE)

Keine Angabe

Kontakt


TEL 12-4

Klös, Verena

lehre@sese.tu-berlin.de

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:

LehrveranstaltungenArtNummerTurnusSpracheSWSVZ
Verifikation von C-Programmen in der PraxisIV0434 L 196SoSeEnglisch2

Arbeitsaufwand und Leistungspunkte

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

AufwandbeschreibungMultiplikatorStundenGesamt
2 Verifikations Aufgaben2.010.0h20.0h
Multiple Choice1.02.0h2.0h
Präsenzzeit3.08.0h24.0h
Vor-/Nachbereitung1.044.0h44.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:

Dieses Modul hat keine Prüfungsvoraussetzungen.

Abschluss des Moduls

Benotung

benotet

Prüfungsform

Portfolioprüfung

Art der Portfolioprüfung

100 Punkte insgesamt

Sprache

Deutsch

Prüfungselemente

NamePunkteKategorieDauer/Umfang
(Ergebnisprüfung) 2 Verifikationsaufgaben mit je 40 Punkten80praktisch2*10h=20h
(Punktuelle Leistungsabfrage) Multiple Choice Aufgabe20schriftlich30-60min

Notenschlüssel

Notenschlüssel »Notenschlüssel 2: Fak IV (2)«

Gesamtpunktzahl1.01.31.72.02.32.73.03.33.74.0
100.0pt95.0pt90.0pt85.0pt80.0pt75.0pt70.0pt65.0pt60.0pt55.0pt50.0pt

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:

Studiengang / StuPOStuPOsVerwendungenErste VerwendungLetzte Verwendung
Dieses Modul findet in keinem Studiengang Verwendung.

Sonstiges

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