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

Vorlesungsfolien

• 22.10.2019: Einführung
• 29.10.2019: Algebraische und logische Grundlagen
• 05.11.2019: Aussagenlogische Erfüllbarkeit
• 12.11.2019: Lineare ganzzahlige Arithmetik
• 19.11.2019: Einführung SMT
• 26.11.2019: SMT, DPLL(T)
• 03.12.2019: Uninterpretierte Funktionen (1. Teil)
• 10.12.2019: Uninterpretierte Funktionen (2. Teil) [Folien siehe 1. Teil]
• 17.12.2019: Bit-Vektor-Logik
• 07.01.2020: Logik der Arrays
• 14.01.2020: Modulare Arithmetik
• 21.01.2020: Kombination von Entscheidungsverfahren
• 28.01.2020: Quantoren-Elimination, Cylindrical Algebraic Decomposition
• 04.02.2020: Statische Software-Analyse

Übungsblätter

• 05.11.2019: Übungsblatt 1
• 18.11.2019: Übungsblatt 2
• 02.12.2019: Übungsblatt 3
• 19.12.2019: Übungsblatt 4
• 20.01.2020: Übungsblatt 5
• 27.01.2020: Übungsblatt 6