CS738 : Concepts, Algorithms and Tools for Model-Checking 2019

Instructors : Ashutosh Gupta and S. Akshay

Timings : 14:00 Monday and Thursday
Venue : CC101

Source material

Evaluation structure

May change later.

Lectures

Introduction

2019-01-03 : Lecture 1 - Introduction to course and program semantics

Model checking : CEGAR

2019-01-07 : Lecture 2 - Aggregate semantics

2019-01-10 : Lecture 3 - Hoare logic and reachability

2019-01-14 : Lecture 4 - Abstractions and CEGAR

2019-01-17 : Lecture 5 - Variants of CEGAR

Verification Tool chain

2019-01-21 : Lecture 6 - LLVM infrastructure

2019-01-24 : Lecture 7 - Building verification tool

Concurrency

2019-01-28 : Lecture 8 - Principles of concurrent programming and mutual exclusion

2019-01-31 : Lecture 9 - mutual exclusion protocols

2019-02-04 : Lecture 10 - Concurrent objects

2019-02-11 : Lecture 11 - Lock-free concurrent objects

Verification of concurrent programs

2019-02-14 : Lecture 12 - Proof systems

2019-02-18 : Lecture 13 - Model-checking concurrent programs

2019-02-21 : Lecture 14 - Proving linearizability

2019-02-21 : Lecture 15 - Weak-memory models

2018-02-22 : (Midterm exam week)


Last modified: ()