Proseminar im Sommersemester 2017
Deduktive Software-Verifikation
Das KeY-Buch
| Veranstaltungstyp: | Proseminar |
|---|---|
| Veranstaltungsnr.: | 2400070 |
| Zielgruppe: | Bachelor Informatik |
| Dozierende: |
Prof. B. Beckert (BB) |
| 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 AuftaktveranstaltungThemenauswahl
| # | 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 |