Endowed professorship for reliable software systems in the automotive industry
Endowed professorship for reliable software systems in the automotive industry
Endowed professorship for reliable software systems in the automotive industry
Endowed professorship for reliable software systems in the automotive industry
Lehrveranstaltungen

Entscheidungsverfahren mit Anwendungen in der Softwareverifikation

  • type:
  • semester: WS 19/20
  • time: 15.10.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


    16.10.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    22.10.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    23.10.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    29.10.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    30.10.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    05.11.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    06.11.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    12.11.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    13.11.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    19.11.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    20.11.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    26.11.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    27.11.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    03.12.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    04.12.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    10.12.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    11.12.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    17.12.2019
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    18.12.2019
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    07.01.2020
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    08.01.2020
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    14.01.2020
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    15.01.2020
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    21.01.2020
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    22.01.2020
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    28.01.2020
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    29.01.2020
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    04.02.2020
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

    05.02.2020
    15:45 - 17:15 wöchentlich
    50.34 Raum 301
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
  • lecturer: Markus Iser
    Prof. Dr. Carsten Sinz
  • sws: 3
  • lv-no.: 2400073
Beschreibung

Entscheidungsverfahren sind Algorithmen, die für ein gegebenes Problem immer eine korrekte Ja/Nein-Antwort liefern.

Sie spielen in der Softwareverifikation eine entscheidende Rolle, da sich mit ihrer Hilfe eine Vielzahl von Korrektheitseigenschaften (z.B. in Bezug auf Speicherzugriffsfehler, Überläufe oder funktionale Eigenschaften) überprüfen und vollautomatisch beweisen lassen.

Die Vorlesung stellt eine Reihe von logischen Entscheidungsverfahren und ihre Anwendung in der automatischen Programmverifikation vor.

Themen sind unter anderem:

  • SAT-Solving, DPLL
  • DPLL(T)
  • Gleichheit mit uninterpretierten Funktionen, Kongruenzabschluß
  • Lineare Arithmetik ganzer Zahlen
  • Bitvektoren und Machinenarithmetik
  • Arrays
  • Quantoren, Quantorenelimination
  • Software Bounded Model Checking
  • Symbolic Execution
  • Predicate Abstraction
  • Werkzeuge: LLBMC, KLEE, SatAbs
Arbeitsbelastung

2 SWS Vorlesung + 1 SWS Übungen

(Vor- und Nachbereitungszeiten: 4h/Woche für Vorlesung plus 2h/Woche für Übungen; Prüfungsvorbereitung: 15h)

Gesamtaufwand:
(2 SWS + 1 SWS + 4 SWS + 2 SWS) x 15h + 15h Prüfungsvorbereitung = 9x15h + 15h = 150h = 5 ECTS