This one of the courses at the Lipa Summer School.

#### Moshe Vardi

*Linear-time verification and synthesis
*

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.