The course introduces automatic verification of systems via model checking. 
We will review different ways to model systems and their properties (specifications) in a formal manner using formulas in temporal logic. 
We will present Model Checking algorithms, discuss their limitations and present several methods for tackling them. In particular, we will define order and equivalence relations between models, we will talk about counterexample-guided abstraction refinement, modular verification, symbolc model checking based on BDDs and based on SAT. We will present algorithms based on interpolation and property directed reachability.