Model Checking and Systems Verification |
Instructors: M. K. Srivas and B. Srivathsan |
January - April 2016 |
| Lectures | Mon 15:30 - 16:45 | Lecture Hall 4 |
| Fri 14:00 - 15:15 | Lecture Hall 4 |
| Lecture 1 | 04.01.2016 (Mon) | Introduction to Model-Checking (Srivathsan) |
|
Chapter 1 of [1] | |||
| Lecture 2 | 08.01.2016 (Fri) | Modeling code behaviour (Srivathsan) | Slides | Pages 19-53 of [1] | |||
| Lecture 3 | 11.01.2016 (Mon) | Model-checker NuSMV (Srivathsan) |
|
||||
| Lecture 4 | 18.01.2016 (Mon) | Checking properties in NuSMV (Srivathsan) |
|
||||
| Lecture 5 | 22.01.2016 (Fri) | Linear Temporal Logic (Srivathsan) | Slides | Sections 5.1.1-5.1.3 of [1] | |||
| Lecture 6 | 25.01.2016 (Mon) | Büchi automata (Srivathsan) | Slides | ||||
| Lecture 7 | 30.01.2016 (Fri) | LTL Illustration (Srivas) | |||||
| Lecture 8 | 30.01.2016 (Fri) | Classification of linear-time properties (Srivas) |
|
||||
| Guest Lecture | 05.02.2016 (Mon) | Probabilistic programming by Joost-Pieter Katoen | |||||
| Lecture 9 | 08.02.2016 (Mon) | Algorithms for LTL (Srivathsan) | Slides | ||||
| Lecture 10 | 12.02.2016 (Fri) | More on LTL model checking (Srivas) | |||||
| Lecture 11 | 15.02.2016 (Mon) | Introduction to symbolic model checking (Srivas) | |||||
| Lecture 12 | 19.02.2016 (Fri) | BDDs: Binary Decision Diagrams (Srivas) |
Intro
slides Ordered BDDs |
Additional reference: NPTEL video by Srivathsan Intro Video Ordered BDDs Video |
|||
| 29.02.2016 (Mon) | Mid-semester Examination | ||||||
| Lecture 13 | 4.03.2016 (Fri) | Operations on BDDs (Srivas) |
Transition
systems as BDDs |
Video | |||
| Lecture 14 | 7.03.2016 (Mon) | Computation Tree Logic (CTL) (Srivathsan) |
Tree
view of a Transition system CTL* CTL |
Video1 Video2 Video3 |
|||
| Lecture 15 | 11.03.2016 (Mon) | Algorithm for CTL (Srivathsan) |
Adequate
CTL formulas EX, EU and EG Final algorithm |
Video1 Video2 Video3 |