Seminar im Sommersemester 2017

Deduktive Software-Verifikation

Von der Theorie zur Anwendung

Veranstaltungstyp: Seminar
Veranstaltungsnr.: 2500005
Zielgruppe: Master/Diplom Informatik
Dozenten:

Prof. B. Beckert (BB)
Sarah Grebing (SaG)
Simon Greiner (SG)
Mihai Herda (MH)
Michael Kirsten (MK)
Dr. Mattias Ulbrich (MU)
Alexander Weigl (AW)

Umfang: 2 SWS / 3 ECTS
Termine: 02.05.2017, 13-14 Uhr in Raum 236 im Gebäude 50.34, Auftaktveranstaltung
12.06.2017, 17:30 - 19:00 Uhr in SR 236 (Gebäude 50.34), Zwischenvorträge
10.07.2017, 17:30 - 19:00 Uhr in SR 236 (Gebäude 50.34), Hauptvorträge
12.07.2017, 11:30 - 13:00 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
14.07.2017, 13:15 - 15:30 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
14.07.2017, 15:45 - 17:15 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
Anmeldung: Persönlich oder per E-Mail bei Simone Meinhart (Raum 223, Gebäude 50.34 bzw. simone meinhartXwx3∂kit edu)
Platzvergabe: Reihenfolge nach Eingang der Anmeldung

Thema

An unserem Lehrstuhl werden formale Methoden für ein weites Spektrum an Problemen in der Softwaresicherheit und -entwicklung erforscht. In diesem Seminar werden formale Methoden vorgestellt, die praxisnahe Probleme vermeiden, optimieren oder verhindern. Die Grundlage für einen Großteil der Themen bildet das Buch Deductive Software Verification – The KeY Book (From Theory to Practice.).

Aufgabenstellung

Bestandteile einer erfolgreichen Teilnahme am Seminar sind eine fünfminütige Kurzpräsentation der Gliederung, der 30-minütige Hauptvortrag, sowie eine etwa zehnseitige Ausarbeitung. Für jeden Vortrag sind von dem/der Studierenden folgende Aufgaben zu erledigen:
  • Verstehen des Stoffes.
  • Auswahl der Themen, die in dem Vortrag präsentiert werden sollen.
  • Entscheidung, wie die Themen präsentiert werden sollen.
  • Erstellung der Folien für die Präsentation und gegebenfalls anderer Materialien.
  • Der Vortrag selbst.

Folien

Folien der Auftaktveranstaltung

Vortragsthemen

# Kapitel Name Betreuung
1 2 First-Order Logic for Java AW
2 3 Dynamic Logic for Java AW
3 6 Abstract Interpretation MK
4 8 From Specification to Proof Obligations MU
5 9 Modular Specification and Verification MU
6 13 Information Flow Analysis SG