Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

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

Literatur

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