Entscheidungsverfahren sind Algorithmen, die für ein gegebenes Entscheidungsproblem 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.

Insbesondere betrachten wir Entscheidungsverfahren für:

• Aussagenlogik
• Logik mit Gleichheit und uninterpretierten Funktionen
• Lineare Arithmetik
• Bit-Vektoren
• Arrays
• Pointer-Logik
• Kombination verschiedener Logiken
• Quantifizierte Boolesche Formeln

Dabei wird, neben den logischen Grundlagen, ein besonderes Augenmerk auf Algorithmen und deren Implementierung liegen.

• Mi 21.10.2009: Vorbesprechung, Einführung ins Thema
• Prüfung: Für die mündliche Prüfung sind die Kapitel 1-4, 6-7, 9 und 11 aus dem Buch "Decision Procedures" relevant.

1. Einführung (21.10.2009), Grundlagen (28.10.2009)
2. Aussagenlogische Erfüllbarkeit / SAT-Solving (04.11.2009)
3. Binäre Entscheidungsdiagramme (18.11.2009)
4. Logik mit Gleichheit und uninterpretierten Funktionen (EUF) (25.11.2009) [1, 2, 3]
5. Entscheidungsverfahren für EUF-Logik (02.12.2009)
6. Bit-Vektor-Logik (09.12.2009)
7. DPLL modulo Theorien (16.12.2009)
8. Arrays und Pointer (13.01.2010)
9. Logik mit Quantoren (20.01.2010, 27.01.2010)
10. Anwendung: Produkt-Konfiguration (03.02.2010)
11. Knuth-Bendix-Vervollständigung (10.02.2010)

• D. Kröning / O. Strichman: Decision Procedures – An Algorithmic Point of View (Springer, 2008)
  [Hinweis: Innerhalb des Uni-Netzes ist eine Online-Version im Volltext verfügbar.]