Proseminar im Sommersemester 2017

Deduktive Software-Verifikation

Das KeY-Buch

Veranstaltungstyp: Proseminar
Veranstaltungsnr.: 2400070
Zielgruppe: Bachelor 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 in 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
Alle Plätze vergeben (10.02.2017)
Neue Anmeldungen kommen auf die Warteliste.

Thema

An unserem Lehrstuhl werden formale Methoden für ein weites Spektrum an Problemen in der Softwaresicherheit und -entwicklung erforscht. In diesem Proseminar 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 Proseminar 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

Themenauswahl

# Kapitel Name Betreuung
1 5 Theories SG
2 7 Formal Specification with the Java Modeling Language MH
3 11 Debugging and Visualization SaG
4 12 Proof-based Test Case Generation MH
5 17 KeY-Hoare SaG
6 19 Verification of Counting Sort and Radix Sort MK