| S.No |
Topic | Videos | Slides | Resources | Evaluation |
|---|---|---|---|---|---|
| 0 | Welcome | Lec 0 (6m45s) | |||
| 1 | Introduction to program reasoning (covers what is reasoning and techniques used) |
Lec 1.1 (8m31s) Lec 1.2 (11m9s) |
Intro | Quiz-1 Assignment-1 |
|
| 2 | What makes program reasoning hard? (covers unhealthy coding practices) |
Lec 2.1 (8m39s) Lec 2.2 (6m43s) Lec 2.3 (9m18s) |
Don'ts | Assignment-2 Viva-1 start |
|
| 3 | Levels of program correctness (explains different levels of correctness with examples and how they are accomplished) |
Lec 3.1 (10m22s) Lec 3.2 (10m10s) Lec 3.3 (6m21s) Lec 3.4 (8m12s) Lec 3.5 (6m) |
Levels of correctness |
Quiz-2 Assignment-3 |
|
| 4 | Towards reasoning of program logic (covers why formal reasoning is important) |
Lec 4.1 (8m43s) Lec 4.2 (8m49s) Lec 4.3 (7m9s) Lec 4.4 (5m3s) Lec 4.5 (9m34s) |
Logic reasoning |
Assignment-4 | |
| 5 | Weakest pre-conditions - 1 (covers calculus associated with primitive types & no loops) |
Lec 5.1 (10m44s) Lec 5.2 (9m5s) Lec 5.3 (7m) Lec 5.4 (14m57s) Lec 5.5 (9m15s) |
Weakest precondition |
Quiz-3 Assignment-5 |
|
| 6 | Getting ready to work with frama-c (covers pre-requisites and guidelines for installing frama-c) |
Lec 6.1(1m19s) | Ubuntu on Windows |
||
| 7 | ANSI C Specification Language (ACSL) (provides an overview of ACSL) |
Lec 7.1 (8m1s) Lec 7.2 (7m44s) Lec 7.3 (13m) |
ACSL | Quiz-4 | |
| 8 | Functional verification with frama-c (covers demonstration of various features of frama-c with suitable examples) |
Lec 8.1 (10m56s) Lec 8.2 (12m30s) Lec 8.3 (9m23s) Lec 8.4 (6m3s) Lec 8.5 (8m24s) Lec 8.6 (10m43s) Lec 8.7 (10m46s) |
Frama-c | Assignment-6 Viva-1 end |
|
| S.No | Topic | Videos | Slides | Resources | Evaluation |
|---|---|---|---|---|---|
| 9 | In prescribed book, read through chapter 3 and try out examples and exercises. |
||||
| 10 | Dealing with loops |
Lec 10.1 () Lec 10.2 () Lec 10.3 () Lec 10.4 () Lec 10.5 () Lec 10.6 () Lec 10.7 () Lec 10.8 () |
10-Loops | ||
| 11 | Program verification on immutable arrays in frama-c (Covers programs on arrays that do not modify elements) |
Lec 11.1 () Lec 11.2 () Lec 11.3 () Lec 11.4 () Lec 11.5 () Lec 11.6 () Lec 11.7 () Lec 11.8 () |
11-Arrays | ||
| 12 | Program verification on mutable arrays in frama-c (Covers programs on arrays that modifies elements) |
Lec 12.1 () Lec 12.2 () Lec 12.3 () Lec 12.4 () |
12-mArrays | ||
| 13 | Program verification with nested loops in frama-c |
||||
| 14 | An overview of how proof systems work |
||||
| 15 | Limits of functional verification | ||||
| S.No | Topic | Videos | Slides | Resources | Activities |
|---|---|---|---|---|---|
| 16 | Concurrency and its problems (Race conditions, safety, liveness, fairness) |
Lec 13.1 () Lec 13.2 () Lec 13.3 () Lec 13.4 () Lec 13.6 () Lec 13.7 () Lec 13.8 () Lec 13.9 () Lec 13.10 () |
13-Threads | ||
| 10 | Classical examples of concurrency (Producer-consumer, readers-writer, dining philosophers, ...) |
14-Examples | |||
| 11 | Behavioral verification (Modelling, temporal properties, model-checking) |
Lec 15.1 () Lec 15.2 () Lec 15.3 () Lec 15.4 () Lec 15.5 () |
15-Model-Checking | ||
| 12 | Property specification using Linear-time Temporal Logic (Covers X, F, G, U, R properties with examples) |
Lec 16.1 () Lec 16.2 () Lec 16.3 () Lec 16.4 () Lec 16.5 () |
16-Temporal-Logic | ||
| 13 | Modeling with Promela: Demo |
||||
| 14 | Model checking with SPIN: Demo |
||||
| 15 | Conclusion | ||||