Modules / Lectures


New Assignments
Module NameDownload
noc18_cs49_Assignment - 8 noc18_cs49_Assignment - 8
noc18_cs49_Assignment1noc18_cs49_Assignment1
noc18_cs49_Assignment10noc18_cs49_Assignment10
noc18_cs49_Assignment11noc18_cs49_Assignment11
noc18_cs49_Assignment12noc18_cs49_Assignment12
noc18_cs49_Assignment2noc18_cs49_Assignment2
noc18_cs49_Assignment3noc18_cs49_Assignment3
noc18_cs49_Assignment4noc18_cs49_Assignment4
noc18_cs49_Assignment6noc18_cs49_Assignment6
noc18_cs49_Assignment7noc18_cs49_Assignment7
noc18_cs49_Assignment9noc18_cs49_Assignment9
noc18_cs49_assignment5noc18_cs49_assignment5


Sl.No Chapter Name MP4 Download
1Course OverviewDownload
2Module 1: Modeling code behaviourDownload
3Module 2: Modeling hardware circuitsDownload
4Module 3: Modeling data-dependent programsDownload
5Module 4: Modeling concurrent systemsDownload
6SummaryDownload
7Module 1: Model checking toolsDownload
8Module 2: Simple models in NuSMVDownload
9Module 3: Hardware verification using NuSMVDownload
10Module 4: Modeling concurrent systems in NuSMVDownload
11Summary.Download
12Module 1: A problem in concurrencyDownload
13Module 2: What is a property?Download
14Module 3: InvariantsDownload
15Module 4: Safety propertiesDownload
16Module 5: Liveness propertiesDownload
17Summary..Download
18Module 1: Road mapDownload
19Module 2: A gentle introduction to automataDownload
20Module 3: Simple properties of finite automataDownload
21Module 4: Safety properties described by automataDownload
22Summary...Download
23Module 1: Specifying propertiesDownload
24Module 2: Omega-regular expressionsDownload
25Module 3: Bchi automataDownload
26Module 4: Simple properties of Bchi automataDownload
27Summary....Download
28Module 1: OverviewDownload
29Module 2: Omega-regular expressions to NBADownload
30Module 3: Checking emptiness of NBADownload
31Module 4: Generalized NBADownload
32Summary.....Download
33Module 1: Introduction to LTLDownload
34Module 2: Semantics of LTLDownload
35Module 3: A puzzleDownload
36Summary .Download
37Module 1: Automata based LTL model-checkingDownload
38Module 2: LTL to NBADownload
39Module 3: Automaton constructionDownload
40Summary ..Download
41Module 1: Tree view of a transition systemDownload
42Module 2: CTL*Download
43Module 3: CTLDownload
44summary ...Download
45Module 1: Adequate CTL formulaeDownload
46Module 2: EX, EU, EGDownload
47Module 3: Final algorithmDownload
48Module 4: State-space explosionDownload
49Summary ....Download
50Module 1: Introduction to BDDsDownload
51Module 2: Ordered BDDsDownload
52Module 3: Representing transition systems as OBDDsDownload
53Summary .....Download
54Timed transition systemsDownload
55Concluding remarksDownload

Sl.No Chapter Name English
1Course OverviewDownload
Verified
2Module 1: Modeling code behaviourDownload
Verified
3Module 2: Modeling hardware circuitsDownload
Verified
4Module 3: Modeling data-dependent programsDownload
Verified
5Module 4: Modeling concurrent systemsDownload
Verified
6SummaryDownload
Verified
7Module 1: Model checking toolsDownload
Verified
8Module 2: Simple models in NuSMVDownload
Verified
9Module 3: Hardware verification using NuSMVDownload
Verified
10Module 4: Modeling concurrent systems in NuSMVDownload
Verified
11Summary.Download
Verified
12Module 1: A problem in concurrencyDownload
Verified
13Module 2: What is a property?Download
Verified
14Module 3: InvariantsDownload
Verified
15Module 4: Safety propertiesDownload
Verified
16Module 5: Liveness propertiesDownload
Verified
17Summary..Download
Verified
18Module 1: Road mapDownload
Verified
19Module 2: A gentle introduction to automataDownload
Verified
20Module 3: Simple properties of finite automataDownload
Verified
21Module 4: Safety properties described by automataDownload
Verified
22Summary...Download
Verified
23Module 1: Specifying propertiesDownload
Verified
24Module 2: Omega-regular expressionsDownload
Verified
25Module 3: Bchi automataDownload
Verified
26Module 4: Simple properties of Bchi automataDownload
Verified
27Summary....Download
Verified
28Module 1: OverviewDownload
Verified
29Module 2: Omega-regular expressions to NBADownload
Verified
30Module 3: Checking emptiness of NBADownload
Verified
31Module 4: Generalized NBADownload
Verified
32Summary.....Download
Verified
33Module 1: Introduction to LTLDownload
Verified
34Module 2: Semantics of LTLDownload
Verified
35Module 3: A puzzleDownload
Verified
36Summary .Download
Verified
37Module 1: Automata based LTL model-checkingDownload
Verified
38Module 2: LTL to NBADownload
Verified
39Module 3: Automaton constructionDownload
Verified
40Summary ..Download
Verified
41Module 1: Tree view of a transition systemDownload
Verified
42Module 2: CTL*Download
Verified
43Module 3: CTLDownload
Verified
44summary ...Download
Verified
45Module 1: Adequate CTL formulaeDownload
Verified
46Module 2: EX, EU, EGDownload
Verified
47Module 3: Final algorithmDownload
Verified
48Module 4: State-space explosionDownload
Verified
49Summary ....Download
Verified
50Module 1: Introduction to BDDsDownload
Verified
51Module 2: Ordered BDDsDownload
Verified
52Module 3: Representing transition systems as OBDDsDownload
Verified
53Summary .....Download
Verified
54Timed transition systemsDownload
Verified
55Concluding remarksDownload
Verified


Sl.No Language Book link
1EnglishNot Available
2BengaliNot Available
3GujaratiNot Available
4HindiNot Available
5KannadaNot Available
6MalayalamNot Available
7MarathiNot Available
8TamilNot Available
9TeluguNot Available