# 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.

## References

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

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