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)
Vorlesungsfolien
- Automaten (27.04.2009/04.05.2009/11.05.2009)
- Temporale Logiken (11.05.2009/18.05.2009/25.05.2009)
- CTL/LTL Model Checking (25.05.2009/18.06.2009)
- Binäre Entscheidungsdiagramme (08.06.2009)
- Symbolic Model Checking (18.06.2009)
- SAT-Solving (22.06.2009)
- Bounded Model Checking (29.06.2009)
- Software Bounded Model Checking (06.07.2009/13.07.2009)
- Anwendungen (20.07.2009)