This one of the courses at the Lipa Summer School.
Algorithmic verification is one of the most successful applications of automated reasoning in computer science. In algorithmic
verification one uses algorithmic techniques to establish the correctness of the system under verification with respect to a given
property. Automama-theoretic Model checking is an algorithmic-verification technique that is based on a small number of key ideas, tying together graph theory, automata theory, and logic. In this self-contained tutorial I will describe how this “holy trinity” gave rise to algorithmic-verification tools, and discuss its applicability to both finite-state and infinite-state systems.