Home | deutsch  | Legals | Sitemap | KIT

Model Checking

Model Checking
type: lecture
place: seminar room 131
time:

Mon. 11:30-13:15

start: 20.04.2009
lecturer:

Ph.D. C. Sinz

sws: 2
lv-no.: 24663
exam:

oral

lecture content

  • 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)

Organizational

  • 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.