This page in EN

Veranstaltung

Entscheidungsverfahren mit Anwendungen in der Softwareverifikation [WS202400073]

Typ
Vorlesung / Übung (VÜ)
Online
Semester
WS 20/21
SWS
3
Sprache
Deutsch
Termine
30
Links
ILIAS

Dozent/en

Einrichtung

  • ITI Sinz

Bestandteil von

Veranstaltungstermine

  • 03.11.2020 12:00 - 13:30
  • 04.11.2020 16:00 - 17:30
  • 10.11.2020 12:00 - 13:30
  • 11.11.2020 16:00 - 17:30
  • 17.11.2020 12:00 - 13:30
  • 18.11.2020 16:00 - 17:30
  • 24.11.2020 12:00 - 13:30
  • 25.11.2020 16:00 - 17:30
  • 01.12.2020 12:00 - 13:30
  • 02.12.2020 16:00 - 17:30
  • 08.12.2020 12:00 - 13:30
  • 09.12.2020 16:00 - 17:30
  • 15.12.2020 12:00 - 13:30
  • 16.12.2020 16:00 - 17:30
  • 22.12.2020 12:00 - 13:30
  • 23.12.2020 16:00 - 17:30
  • 12.01.2021 12:00 - 13:30
  • 13.01.2021 16:00 - 17:30
  • 19.01.2021 12:00 - 13:30
  • 20.01.2021 16:00 - 17:30
  • 26.01.2021 12:00 - 13:30
  • 27.01.2021 16:00 - 17:30
  • 02.02.2021 12:00 - 13:30
  • 03.02.2021 16:00 - 17:30
  • 09.02.2021 12:00 - 13:30
  • 10.02.2021 16:00 - 17:30
  • 16.02.2021 12:00 - 13:30
  • 17.02.2021 16:00 - 17:30
  • 01.03.2021 10:00 - 14:45 - Room: 50.34 Raum 236
  • 29.03.2021 10:00 - 15:30 - Room: 50.34 Raum 236

Anmerkung

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

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