Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

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