|
Part 1: Automata theoretic approach to model
checking (Instructor: Srivathsan)
|
|
|
|
Course overview, Modeling code behaviour as
transition systems
|
|
|
Chapter 1 of [1]
|
|
|
|
Modeling concurrent systems
|
|
Introduction to NuSMV
|
|
|
|
|
|
|
Continuation of NuSMV
|
|
Formalizing the notion of "properties of a system"
|
|
|
|
|
|
|
Classification of Linear time properties
|
|
A particular class: regular properties
|
|
|
|
|
|
|
Büchi automata; Closure properties,
deterministic vs non-deterministic Büchi automata
|
|
|
|
|
|
|
|
|
|
|
|
Complementing Büchi automata
|
|
|
Section 2 of Prof Kumar's Notes
|
|
|
|
|
|
|
|
|
|
|
|
|
| Lecture 10 |
| (05. 02. 2018) |
|
|
Computation Tree Logics CTL, CTL*; comparison with LTL
|
|
|
|
| Lecture 11 |
| (12. 02. 2018) |
|
|
|
|