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 18/19
  • time: 16.10.2018
    11:30 - 13:00 wöchentlich
    50.34 Raum 236
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    06.02.2019
    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