Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

Entscheidungsverfahren mit Anwendungen in der Softwareverifikation

  • Typ: Vorlesung (V)
  • Semester: SS 2013
  • Ort:

    50.34 Raum 131

  • Zeit:

    Mo 14:00-15:30

  • Beginn: 15.04.2013
  • Dozent: Dr. Carsten Sinz
    Dr. Stephan Falke
  • SWS: 2
  • ECTS: 3
  • LVNr.: 2400034

Vorlesungsinhalte

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 automatische Programmverifikation vor.

Themen sind unter anderem:

  • SAT-Solving, DPLL
  • SMT, DPLL(T)
  • Gleichheit mit uninterpretierten Funktionen, Kongruenzabschluss
  • Lineare Arithmetik ganzer Zahlen
  • Bitvektoren
  • Arrays
  • Kombination von Entscheidungsverfahren
  • Software Bounded Model Checking
  • Symbolic Execution
  • Predicate Abstraction
Darüber hinaus werden wir Werkzeuge der Programmverifikation (wie LLBMC, KLEE, SatAbs) vorstellen und kleine Verifikationsprobleme mit diesen lösen.
 

Folien