Endowed professorship for reliable software systems in the automotive industry

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

Literatur

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