Model Checking and Systems Verification

Instructors:   M. K. Srivas and B. Srivathsan

January - April 2018


Hours

Lectures Mon   14:00 - 15:30 Lecture Hall 804
Thu   14:00 - 15:15 Lecture Hall 804




References

[1] Principles of Model Checking by Christel Baier and Joost-Pieter Katoen (MIT Press 2008)


Additional references and links

[1] NuSMV web page

[2] A nice talk by Leslie Lamport: Thinking for Programmers


Lecture Slides



Part 1: Automata theoretic approach to model checking (Instructor: Srivathsan)
Lecture 1
(04. 01. 2018)
Course overview, Modeling code behaviour as transition systems
Course Overview
Link to F. Herbreteau/Igor Walukiewicz's slides (for reference)
Link to Yogananda Jeppu's slides (for reference)
Slides on modeling code behaviour (Modules 1 - 3)
Chapter 1 of [1]
Lecture 2
(08. 01. 2018)
Modeling concurrent systems
Introduction to NuSMV
Slides (Module 4)
Slides for NuSMV
NuSMV Demo files
Lecture 3
(11. 01. 2018)
Continuation of NuSMV
Formalizing the notion of "properties of a system"
Slides (from Slide 22 -)
Slides
NuSMV Demo files
Lecture 4
(15. 01. 2018)
Classification of Linear time properties
A particular class: regular properties
Slides
Slides