Model Checking and Systems Verification

Instructors:   M. K. Srivas and B. Srivathsan

January - April 2017


Hours

Lectures Mon   15:30 - 16:45 Lecture Hall 6
Fri   11:50 - 13:05 Lecture Hall 4




References

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

[2] Notes by Luke Ong, Oxford University, UK

[3] Notes by Madhavan, Chennai Mathematical Institute, India


Additional references and links

[1] NuSMV web page

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


Tutorials

Tutorial 1     Tutorial 2     Tutorial 3     Tutorial 4


Lecture Slides



Lecture 1 06.03.2017 (Mon) Introduction to omega-languages; Büchi automata; deterministic vs non-deterministic Büchi automata Slides Sections 1.1, 1.2 (except complementation) of [2]
Lecture 2 10.03.2017 (Fri) More on Büchi automata, omega-regular expressions, exercises Section 1.3 of [2]
Lecture 3 17.03.2017 (Fri) Linear Temporal Logic; syntax, semantics and examples Section 2.1, 2.2, 2.3 of [2]
Lecture 4 20.03.2017 (Mon) LTL to Büchi automata Section 2.4 of [2], [3]
Lecture 5 24.03.2017 (Fri) Kripke structures, LTL model checking, reducing 3CNF SAT to LTL model checking Section 2.5 of [2] (except Theorem 2.2)
Lecture 6 27.03.2017 (Mon) Computation Tree Logics CTL, CTL*; comparison with LTL Slides Lemma 6.19 of [1]
Lecture 7 31.03.2017 (Fri) CTL model checking algorithm Slides
Lecture 8 03.04.2017 (Mon) Timed languages and timed automata Slides
Lecture 9 07.04.2017 (Fri) Closure properties of timed languages Slides
Lecture 10 10.04.2017 (Mon) Untiming construction Notes
Lecture 11 12.04.2017 (Wed) Undecidability of language inclusion for timed automata Slides
Lecture 12 14.04.2017 (Fri) Determinizing timed automata; Determinizable subclasses - ERA, IRTA, SNZ (only ERA needed for exam) Slides