Home | english  | Impressum | Sitemap | KIT

Model Checking

Model Checking
Typ: Vorlesung
Ort:

Seminarraum 131 (50.34)

Zeit:

Mo 11:30-13:15

Beginn: 20.04.2009
Dozent:

Dr. C. Sinz

SWS: 2
LVNr.: 24663
Prüfung:

mündlich

Vorlesungsinhalte

  • Automatentheorie, temporale Logiken (LTL, CTL)
  • SAT-Solving und binäre Entscheidungsdiagramme
  • Explicit State Model Checking
  • Symbolic Model Checking
  • Bounded Model Checking
  • Software Bounded Model Checking
  • Werkzeuge: SPIN, SMV, BLAST, CBMC
  • Anwendungen: Hardware-Verifikation, Software-Verifikation (Betriebssysteme, Sicherheitslücken wie Pufferüberläufe, Automobil-Software, Software in mobilen Geräten)

Organisatorisches

  • Mo 20.04.2009: Vorbesprechung, Einführung ins Thema

Vorlesungsfolien

Literatur

  • E. Clarke, O. Grumberg, D. Peled: Model Checking. MIT Press, 1999.
  • K. McMillan: Symbolic Model Checking. Kluwer, 1993.