Model Checking

July to November 2018




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.

References

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
Summary
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
Summary
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
Summary
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
Summary
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
Summary
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
Summary
Unit 7 Linear Temporal Logic
Module 1: Introduction to LTL
Module 2: Semantics of LTL
Module 3: A puzzle
Summary
Unit 8 Algorithms for LTL
Module 1: Automata based LTL model-checking
Module 2: LTL to NBA
Module 3: Automaton construction
Summary
Unit 9 Computation Tree Logic
Module 1: Tree view of a transition system
Module 2: CTL*
Module 3: CTL
Summary
Unit 10 Algorithms for CTL
Module 1: Adequate CTL formulas
Module 2: EX, EU, EG
Module 3: Final algorithm
Module 3: State-space explosion
Summary
Unit 11 Binary Decision Diagrams (BDDs)
Module 1: Introduction to BDDs
Module 2: Ordered BDDs
Module 3: Representing transition systems as BDDs
Summary
Unit 12 Modeling timing constraints
Adding time to transition systems
Concluding remarks