Dynamic logic is a multi-modal logic for reasoning about programs. In deductive verification systems, it can be used as a versatile alternative to the Floyd-Hoare calculus with uniform syntax and semantics. Dynamic logic has not only been used in functional verification, but one can represent a plethora of verification scenarios in it, including relational and hyperproperties, program equivalence, information flow, incorrectness logic. Dynamic logic is the basis for three deductive verification tools that are highly competitive in their application domain. In this article, we present the foundations of dynamic logic and we review its many uses in state-of-the-art deductive verification.