NOC:Model Checking


Lecture 1 - Course Overview


Lecture 2 - Module 1 - Modeling code behaviour


Lecture 3 - Module 2 - Modeling hardware circuits


Lecture 4 - Module 3 - Modeling data-dependent programs


Lecture 5 - Module 4 - Modeling concurrent systems


Lecture 6 - Summary


Lecture 7 - Module 1 - Model checking tools


Lecture 8 - Module 2 - Simple models in NuSMV


Lecture 9 - Module 3 - Hardware verification using NuSMV


Lecture 10 - Module 4 - Modeling concurrent systems in NuSMV


Lecture 11 - Summary.


Lecture 12 - Module 1 - A problem in concurrency


Lecture 13 - Module 2 - What is a property?


Lecture 14 - Module 3 - Invariants


Lecture 15 - Module 4 - Safety properties


Lecture 16 - Module 5 - Liveness properties


Lecture 17 - Summary..


Lecture 18 - Module 1 - Road map


Lecture 19 - Module 2 - A gentle introduction to automata


Lecture 20 - Module 3 - Simple properties of finite automata


Lecture 21 - Module 4 - Safety properties described by automata


Lecture 22 - Summary...


Lecture 23 - Module 1 - Specifying properties


Lecture 24 - Module 2 - Omega-regular expressions


Lecture 25 - Module 3 - Bchi automata


Lecture 26 - Module 4 - Simple properties of Bchi automata


Lecture 27 - Summary....


Lecture 28 - Module 1 - Overview


Lecture 29 - Module 2 - Omega-regular expressions to NBA


Lecture 30 - Module 3 - Checking emptiness of NBA


Lecture 31 - Module 4 - Generalized NBA


Lecture 32 - Summary.....


Lecture 33 - Module 1 - Introduction to LTL


Lecture 34 - Module 2 - Semantics of LTL


Lecture 35 - Module 3 - A puzzle


Lecture 36 - Summary.


Lecture 37 - Module 1 - Automata based LTL model-checking


Lecture 38 - Module 2 - LTL to NBA


Lecture 39 - Module 3 - Automaton construction


Lecture 40 - Summary..


Lecture 41 - Module 1 - Tree view of a transition system


Lecture 42 - Module 2 - CTL*


Lecture 43 - Module 3 - CTL


Lecture 44 - summary...


Lecture 45 - Module 1 - Adequate CTL formulae


Lecture 46 - Module 2 - EX, EU, EG


Lecture 47 - Module 3 - Final algorithm


Lecture 48 - Module 4 - State-space explosion


Lecture 49 - Summary....


Lecture 50 - Module 1 - Introduction to BDDs


Lecture 51 - Module 2 - Ordered BDDs


Lecture 52 - Module 3 - Representing transition systems as OBDDs


Lecture 53 - Summary.....


Lecture 54 - Timed transition systems


Lecture 55 - Concluding remarks