Modules / Lectures
Module NameDownloadDescriptionDownload Size
Introduction to model checkingWeek 1 AssignmentWeek 1 Assignment 1153 kb
Introduction to model checkingAssignment IAssignment I Solutions6 kb
Introduction to model checkingAssignment IAssignment I Questions19 kb
Model checker NuSMVWeek 2 AssignmentWeek 2 Assignment 1177 kb
Linear-time propertiesWeek 3 AssignmentWeek 3 Assignment 1172 kb
Linear-time propertiesAssignment IIAssignment II Solutions45 kb
Linear-time propertiesAssignment IIAssignment II Questions97 kb
Regular propertiesAssignment IIIAssignment III Questions118 kb
Regular propertiesAssignment IIIAssignment III Solutions145 kb
Regular propertiesWeek 4 AssignmentWeek 4 Assignment 1236 kb
Omega-regular propertiesAssignment IVAssignment IV Questions32 kb
Omega-regular propertiesAssignment IVAssignment IV Solutions118 kb
Omega-regular propertiesWeek 5 AssignmentWeek 5 Assignment 1241 kb
Model-checking omega-regular propertiesWeek 6 AssignmentWeek 6 Assignment 1178 kb
Linear Temporal LogicWeek 7 AssignmentWeek 7 Assignment 1136 kb
Algorithms for LTLAssignment VAssignment V Questions32 kb
Algorithms for LTLAssignment VAssignment V Solutions8 kb
Algorithms for LTLWeek 8 AssignmentWeek 8 Assignment 1165 kb
Computation Tree LogicWeek 9 AssignmentWeek 9 Assignment 1147 kb
Algorithms for CTLWeek 10 AssignmentWeek 10 Assignment 1154 kb
Binary Decision Diagrams (BDDs)Week 11 AssignmentWeek 11 Assignment 1227 kb
Modeling timing constraintsWeek 12 AssignmentWeek 12 Assignment 1153 kb


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 Transcript Download
1Course OverviewDownloadDownload
Verified
2Module 1: Modeling code behaviourDownloadDownload
Verified
3Module 2: Modeling hardware circuitsDownloadDownload
Verified
4Module 3: Modeling data-dependent programsDownloadDownload
Verified
5Module 4: Modeling concurrent systemsDownloadDownload
Verified
6SummaryDownloadDownload
Verified
7Module 1: Model checking toolsDownloadDownload
Verified
8Module 2: Simple models in NuSMVDownloadDownload
Verified
9Module 3: Hardware verification using NuSMVDownloadDownload
Verified
10Module 4: Modeling concurrent systems in NuSMVDownloadDownload
Verified
11Summary.DownloadDownload
Verified
12Module 1: A problem in concurrencyDownloadDownload
Verified
13Module 2: What is a property?DownloadDownload
Verified
14Module 3: InvariantsDownloadDownload
Verified
15Module 4: Safety propertiesDownloadDownload
Verified
16Module 5: Liveness propertiesDownloadDownload
Verified
17Summary..DownloadDownload
Verified
18Module 1: Road mapDownloadDownload
Verified
19Module 2: A gentle introduction to automataDownloadDownload
Verified
20Module 3: Simple properties of finite automataDownloadDownload
Verified
21Module 4: Safety properties described by automataDownloadDownload
Verified
22Summary...DownloadDownload
Verified
23Module 1: Specifying propertiesDownloadDownload
Verified
24Module 2: Omega-regular expressionsDownloadDownload
Verified
25Module 3: Bchi automataDownloadDownload
Verified
26Module 4: Simple properties of Bchi automataDownloadDownload
Verified
27Summary....DownloadDownload
Verified
28Module 1: OverviewDownloadDownload
Verified
29Module 2: Omega-regular expressions to NBADownloadDownload
Verified
30Module 3: Checking emptiness of NBADownloadDownload
Verified
31Module 4: Generalized NBADownloadDownload
Verified
32Summary.....DownloadDownload
Verified
33Module 1: Introduction to LTLDownloadDownload
Verified
34Module 2: Semantics of LTLDownloadDownload
Verified
35Module 3: A puzzleDownloadDownload
Verified
36Summary .DownloadDownload
Verified
37Module 1: Automata based LTL model-checkingDownloadDownload
Verified
38Module 2: LTL to NBADownloadDownload
Verified
39Module 3: Automaton constructionDownloadDownload
Verified
40Summary ..DownloadDownload
Verified
41Module 1: Tree view of a transition systemDownloadDownload
Verified
42Module 2: CTL*DownloadDownload
Verified
43Module 3: CTLDownloadDownload
Verified
44summary ...DownloadDownload
Verified
45Module 1: Adequate CTL formulaeDownloadDownload
Verified
46Module 2: EX, EU, EGDownloadDownload
Verified
47Module 3: Final algorithmDownloadDownload
Verified
48Module 4: State-space explosionDownloadPDF unavailable
49Summary ....DownloadPDF unavailable
50Module 1: Introduction to BDDsDownloadPDF unavailable
51Module 2: Ordered BDDsDownloadPDF unavailable
52Module 3: Representing transition systems as OBDDsDownloadPDF unavailable
53Summary .....DownloadPDF unavailable
54Timed transition systemsDownloadPDF unavailable
55Concluding remarksDownloadPDF unavailable