Home | deutsch  | Legals | Sitemap | KIT

Entscheidungsverfahren für die Software-Verifikation

Entscheidungsverfahren für die Software-Verifikation
type: lecture
place: seminar room 301 (building 50.34)
time:

Wed 14:00-15:30

start: 21.10.2009
lecturer:

C. Sinz, O. Tveretina

sws: 2
lv-no.: 24159
exam:

oral

Vorlesungsinhalte

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.

Organisatorisches

  • Mi 21.10.2009: Vorbesprechung, Einführung ins Thema

Vorlesungsfolien

Literatur

  • D. Kröning / O. Strichman: Decision Procedures – An Algorithmic Point of View (Springer, 2008)