| Sl.No | Chapter Name | MP4 Download |
|---|---|---|
| 1 | Course Overview | Download |
| 2 | Module 1: Modeling code behaviour | Download |
| 3 | Module 2: Modeling hardware circuits | Download |
| 4 | Module 3: Modeling data-dependent programs | Download |
| 5 | Module 4: Modeling concurrent systems | Download |
| 6 | Summary | Download |
| 7 | Module 1: Model checking tools | Download |
| 8 | Module 2: Simple models in NuSMV | Download |
| 9 | Module 3: Hardware verification using NuSMV | Download |
| 10 | Module 4: Modeling concurrent systems in NuSMV | Download |
| 11 | Summary. | Download |
| 12 | Module 1: A problem in concurrency | Download |
| 13 | Module 2: What is a property? | Download |
| 14 | Module 3: Invariants | Download |
| 15 | Module 4: Safety properties | Download |
| 16 | Module 5: Liveness properties | Download |
| 17 | Summary.. | Download |
| 18 | Module 1: Road map | Download |
| 19 | Module 2: A gentle introduction to automata | Download |
| 20 | Module 3: Simple properties of finite automata | Download |
| 21 | Module 4: Safety properties described by automata | Download |
| 22 | Summary... | Download |
| 23 | Module 1: Specifying properties | Download |
| 24 | Module 2: Omega-regular expressions | Download |
| 25 | Module 3: Bchi automata | Download |
| 26 | Module 4: Simple properties of Bchi automata | Download |
| 27 | Summary.... | Download |
| 28 | Module 1: Overview | Download |
| 29 | Module 2: Omega-regular expressions to NBA | Download |
| 30 | Module 3: Checking emptiness of NBA | Download |
| 31 | Module 4: Generalized NBA | Download |
| 32 | Summary..... | Download |
| 33 | Module 1: Introduction to LTL | Download |
| 34 | Module 2: Semantics of LTL | Download |
| 35 | Module 3: A puzzle | Download |
| 36 | Summary . | Download |
| 37 | Module 1: Automata based LTL model-checking | Download |
| 38 | Module 2: LTL to NBA | Download |
| 39 | Module 3: Automaton construction | Download |
| 40 | Summary .. | Download |
| 41 | Module 1: Tree view of a transition system | Download |
| 42 | Module 2: CTL* | Download |
| 43 | Module 3: CTL | Download |
| 44 | summary ... | Download |
| 45 | Module 1: Adequate CTL formulae | Download |
| 46 | Module 2: EX, EU, EG | Download |
| 47 | Module 3: Final algorithm | Download |
| 48 | Module 4: State-space explosion | Download |
| 49 | Summary .... | Download |
| 50 | Module 1: Introduction to BDDs | Download |
| 51 | Module 2: Ordered BDDs | Download |
| 52 | Module 3: Representing transition systems as OBDDs | Download |
| 53 | Summary ..... | Download |
| 54 | Timed transition systems | Download |
| 55 | Concluding remarks | Download |
| Sl.No | Chapter Name | English |
|---|---|---|
| 1 | Course Overview | Download Verified |
| 2 | Module 1: Modeling code behaviour | Download Verified |
| 3 | Module 2: Modeling hardware circuits | Download Verified |
| 4 | Module 3: Modeling data-dependent programs | Download Verified |
| 5 | Module 4: Modeling concurrent systems | Download Verified |
| 6 | Summary | Download Verified |
| 7 | Module 1: Model checking tools | Download Verified |
| 8 | Module 2: Simple models in NuSMV | Download Verified |
| 9 | Module 3: Hardware verification using NuSMV | Download Verified |
| 10 | Module 4: Modeling concurrent systems in NuSMV | Download Verified |
| 11 | Summary. | Download Verified |
| 12 | Module 1: A problem in concurrency | Download Verified |
| 13 | Module 2: What is a property? | Download Verified |
| 14 | Module 3: Invariants | Download Verified |
| 15 | Module 4: Safety properties | Download Verified |
| 16 | Module 5: Liveness properties | Download Verified |
| 17 | Summary.. | Download Verified |
| 18 | Module 1: Road map | Download Verified |
| 19 | Module 2: A gentle introduction to automata | Download Verified |
| 20 | Module 3: Simple properties of finite automata | Download Verified |
| 21 | Module 4: Safety properties described by automata | Download Verified |
| 22 | Summary... | Download Verified |
| 23 | Module 1: Specifying properties | Download Verified |
| 24 | Module 2: Omega-regular expressions | Download Verified |
| 25 | Module 3: Bchi automata | Download Verified |
| 26 | Module 4: Simple properties of Bchi automata | Download Verified |
| 27 | Summary.... | Download Verified |
| 28 | Module 1: Overview | Download Verified |
| 29 | Module 2: Omega-regular expressions to NBA | Download Verified |
| 30 | Module 3: Checking emptiness of NBA | Download Verified |
| 31 | Module 4: Generalized NBA | Download Verified |
| 32 | Summary..... | Download Verified |
| 33 | Module 1: Introduction to LTL | Download Verified |
| 34 | Module 2: Semantics of LTL | Download Verified |
| 35 | Module 3: A puzzle | Download Verified |
| 36 | Summary . | Download Verified |
| 37 | Module 1: Automata based LTL model-checking | Download Verified |
| 38 | Module 2: LTL to NBA | Download Verified |
| 39 | Module 3: Automaton construction | Download Verified |
| 40 | Summary .. | Download Verified |
| 41 | Module 1: Tree view of a transition system | Download Verified |
| 42 | Module 2: CTL* | Download Verified |
| 43 | Module 3: CTL | Download Verified |
| 44 | summary ... | Download Verified |
| 45 | Module 1: Adequate CTL formulae | Download Verified |
| 46 | Module 2: EX, EU, EG | Download Verified |
| 47 | Module 3: Final algorithm | Download Verified |
| 48 | Module 4: State-space explosion | Download Verified |
| 49 | Summary .... | Download Verified |
| 50 | Module 1: Introduction to BDDs | Download Verified |
| 51 | Module 2: Ordered BDDs | Download Verified |
| 52 | Module 3: Representing transition systems as OBDDs | Download Verified |
| 53 | Summary ..... | Download Verified |
| 54 | Timed transition systems | Download Verified |
| 55 | Concluding remarks | Download Verified |
| Sl.No | Language | Book link |
|---|---|---|
| 1 | English | Download |
| 2 | Bengali | Not Available |
| 3 | Gujarati | Not Available |
| 4 | Hindi | Not Available |
| 5 | Kannada | Not Available |
| 6 | Malayalam | Not Available |
| 7 | Marathi | Not Available |
| 8 | Tamil | Not Available |
| 9 | Telugu | Not Available |