Seminar im Sommersemester 2017
Deduktive Software-Verifikation
Von der Theorie zur Anwendung
| Veranstaltungstyp: | Seminar |
|---|---|
| Veranstaltungsnr.: | 2500005 |
| Zielgruppe: | Master/Diplom Informatik |
| Dozierende: |
Prof. B. Beckert (BB) |
| 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 AuftaktveranstaltungVortragsthemen
| # | 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 |