Home | english  | Impressum | Datenschutz | Sitemap | KIT

Ausgewählte Kapitel der Algorithmischen Verifikation

Ausgewählte Kapitel der Algorithmischen Verifikation
Typ: Seminar (S)
Semester: WS 19/20
Zeit: 14.10.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


21.10.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

28.10.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

04.11.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

11.11.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

18.11.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

25.11.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

02.12.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

09.12.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

16.12.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

23.12.2019
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

13.01.2020
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

20.01.2020
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

27.01.2020
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

03.02.2020
17:30 - 19:00 wöchentlich
50.34 Raum -109
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


Dozent: Prof. Dr. Carsten Sinz
SWS: 2
LVNr.: 2400092
Beschreibung

Viele sicherheitskritische Systeme sind inzwischen Software-gesteuert und Software-Korrektheit daher essentiell. Andererseits ist es praktisch unmöglich, Eigenschaften eines Systems zu garantieren und die Abwesenheit von Fehlern durch Standard-Softwareengineering-Praktiken wie Code-Review, systematisches Testen und gutes Software-Design allein zu erreichen.

Im Bereich der Formalen Methoden sind jedoch inzwischen verschiedene mathematische Techniken und Werkzeuge verfügbar, die eine automatische Analyse von Systemen und Software ermöglichen.

Die Anwendung dieser vollautomatischen Techniken wird typischerweise algorithmische Verifikation genannt.

In diesem Seminar sollen aktuelle Arbeiten zur algorithmischen Verifikation behandelt werden, insbesondere neue Algorithmen und deren Implementation in vollautomatischen Software-Analyse-Werkzeugen. Es sollen auch Beispiele diskutiert werden, in denen diese Techniken erfolgreich angewandt wurden.

Lehrinhalt

Fachlich soll dieses Seminar Studierende in die Lage versetzen, vollautomatische Verifikationstechniken und die dahinterstehenden Algorithmen in der eigenen Entwicklungstätigkeit einzusetzen und einen Nachweis der Korrektheit von Programmen zu führen.

Neben den inhaltlichen Aspekten sowie Techniken des wissenschaftlichen Arbeitens werden in dieser Veranstaltung auch Schlüsselqualifikationen wie Literaturrecherche und Präsentationstechniken vermittelt.

Arbeitsbelastung

90h = 3 ECTS