Model Checking

July - November 2015

Course description

This course is offered as an NPTEL Massive Open Online course. In this page, slides used in the videos and the solutions to assignments would be uploaded.


Principles of Model Checking by Christel Baier and Joost-Pieter Katoen (MIT Press 2008)

NuSMV demo files

Week2     Week 3

Lecture Slides

Unit 1 Introduction to Model-Checking
Course Overview
Module 1: Modeling code behaviour
Module 2: Modeling hardware circuits
Module 3: Modeling data-dependent programs
Module 4: Modeling concurrent systems
Unit 2 Model-checker NuSMV
Module 1: Model-checking tools
Module 2: Simple models in NuSMV
Module 3: Hardware verification using NuSMV
Module 4: Modeling concurrent systems in NuSMV
Unit 3 Linear-time properties
Module 1: A problem in concurrency
Module 2: What is a property?
Module 3: Invariants
Module 4: Safety properties
Module 5: Liveness
Unit 4 Regular properties
Module 1: Road Map
Module 2: A gentle introduction to automata
Module 3: Simple properties of finite automata
Module 4: Safety properties described by automata
Unit 5 Omega-regular properties
Module 1: Specifying properties
Module 2: Omega-regular expressions
Module 3: Büchi automata
Module 4: Simple properties of Büchi automata
Unit 6 Model checking omega-regular properties
Module 1: Overview
Module 2: Omega-regular expressions to NBA
Module 3: Checking emptiness of NBA
Module 4: Generalized NBA
Unit 7 Linear Temporal Logic
Module 1: Introduction to LTL
Module 2: Semantics of LTL
Module 3: A puzzle
Unit 8 Algorithms for LTL
Module 1: Automata based LTL model-checking
Module 2: LTL to NBA
Module 3: Automaton construction
Unit 9 Computation Tree Logic
Module 1: Tree view of a transition system
Module 2: CTL*
Module 3: CTL
Unit 10 Algorithms for CTL
Module 1: Adequate CTL formulas
Module 2: EX, EU, EG
Module 3: Final algorithm
Module 3: State-space explosion
Unit 11 Binary Decision Diagrams (BDDs)
Module 1: Introduction to BDDs
Module 2: Ordered BDDs
Module 3: Representing transition systems as BDDs
Unit 12 Modeling timing constraints
Adding time to transition systems
Concluding remarks