Modern computing systems typically consist of many components running in parallel, and interacting with each other and their environment. They are not designed to compute a result, but, rather, to execute a process and thus exhibit behavior. For a correct design of a modern computing system, it is therefore essential to be able to specify its intended behavior, at different levels of abstraction, and to analyze and reason about this behavior. This course offers a formal approach to specifying and reasoning about system behavior, and it introduces the algorithmics for analyzing system behavior.