Learn · NPTEL

Course10610613655 lectures

Model Checking

Prof. Srivathsan.B · Chennai Mathematical Institute

Start with lecture 1 At NPTEL

Lectures

Introduction to model checking

  1. Course Overview Video
  2. Module 1: Modeling code behaviour Video
  3. Module 2: Modeling hardware circuits Video
  4. Module 3: Modeling data-dependent programs Video
  5. Module 4: Modeling concurrent systems Video
  6. Summary Video

Model checker NuSMV

  1. Module 1: Model checking tools Video
  2. Module 2: Simple models in NuSMV Video
  3. Module 3: Hardware verification using NuSMV Video
  4. Module 4: Modeling concurrent systems in NuSMV Video
  5. Summary. Video

Linear-time properties

  1. Module 1: A problem in concurrency Video
  2. Module 2: What is a property? Video
  3. Module 3: Invariants Video
  4. Module 4: Safety properties Video
  5. Module 5: Liveness properties Video
  6. Summary.. Video

Regular properties

  1. Module 1: Road map Video
  2. Module 2: A gentle introduction to automata Video
  3. Module 3: Simple properties of finite automata Video
  4. Module 4: Safety properties described by automata Video
  5. Summary... Video

Omega-regular properties

  1. Module 1: Specifying properties Video
  2. Module 2: Omega-regular expressions Video
  3. Module 3: Bchi automata Video
  4. Module 4: Simple properties of Bchi automata Video
  5. Summary.... Video

Model-checking omega-regular properties

  1. Module 1: Overview Video
  2. Module 2: Omega-regular expressions to NBA Video
  3. Module 3: Checking emptiness of NBA Video
  4. Module 4: Generalized NBA Video
  5. Summary..... Video

Linear Temporal Logic

  1. Module 1: Introduction to LTL Video
  2. Module 2: Semantics of LTL Video
  3. Module 3: A puzzle Video
  4. Summary . Video

Algorithms for LTL

  1. Module 1: Automata based LTL model-checking Video
  2. Module 2: LTL to NBA Video
  3. Module 3: Automaton construction Video
  4. Summary .. Video

Computation Tree Logic

  1. Module 1: Tree view of a transition system Video
  2. Module 2: CTL* Video
  3. Module 3: CTL Video
  4. summary ... Video

Algorithms for CTL

  1. Module 1: Adequate CTL formulae Video
  2. Module 2: EX, EU, EG Video
  3. Module 3: Final algorithm Video
  4. Module 4: State-space explosion Video
  5. Summary .... Video

Binary Decision Diagrams (BDDs)

  1. Module 1: Introduction to BDDs Video
  2. Module 2: Ordered BDDs Video
  3. Module 3: Representing transition systems as OBDDs Video
  4. Summary ..... Video

Modeling timing constraints

  1. Timed transition systems Video
  2. Concluding remarks Video

Syllabus and materials

At NPTEL, as the course publishes them.

Credits and licence

Institution
Chennai Mathematical Institute
Department
Computer Science and Engineering
Teacher
Prof. Srivathsan.B
Level
Undergraduate
Language
English
Subjects
Computer science, Engineering
Source
NPTEL
Licence
CC BY-NC-SA, as NPTEL states it. Non-commercial use only. NPTEL's terms
Attribution
NPTEL states: "Distributed under Creative Commons Attribution-ShareAlike / CC BY - NC - SA", beside a BY-NC-SA badge. Coordinated by IIT Madras.
Who can watch
NPTEL gives no rating. Invisible Network shows it to Tweens profiles and older, judged from what the source says about it. How courses are placed