Introduction to Model Checking
for those of you that do not have a background in model checking, I have added a link to a course "Introduction to Model Checking" in the Materials.
To get the basic ideas of system models, Lecture 1 and the first half of Lecture 2 should be enough.
Based on these models, we are interested in safety model checking, which is fairly simple: does there exist a finite trace in the model with certain properties? (in the easiest case: a trace that ends in a state with a certain given label)