Endowed professorship for reliable software systems in the automotive industry

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

Literatur

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