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 nondeterministic 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) 



