NPTEL : NOC:Model Checking (Computer Science and Engineering)

Co-ordinators : Prof. B. Srivathsan


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