Dynamic Logic was developed in the late 1970s by David Harel building on previous work by V.R.Pratt. It is a modal logic and as any modal logic it allows to reason about the truth of statements in different states (or worlds). It extends classical modal logic however by taking explicitly into account the transitions from one state to the next state(s). Descriptions of actions (events, or programs) are part of the syntax of Dynamic Logic. This course will start with an introduction into the logical theory of propositional and first-order dynamic logic with respect to a very fine grained notion of actions. At the next level a Dynamic Logic for an abstract programing language will be considered. We will end by presenting a Dynamic Logic for a real programming language and show how this can be used in software verification including a demo of a working system.