@Inbook{Ahrendt2025,
author="Ahrendt, Wolfgang
and Beckert, Bernhard
and Bubel, Richard
and H{\"a}hnle, Reiner
and Ulbrich, Mattias",
editor="Ernst, Gidon
and G{\"u}demann, Matthias
and Knapp, Alexander
and Nafz, Florian
and Ortmeier, Frank
and Ponsar, Hella
and Schellhorn, Gerhard
and Schiendorfer, Alexander",
title="The Many Uses of Dynamic Logic",
bookTitle="Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="56--82",
abstract="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.",
isbn="978-3-031-92196-4",
doi="10.1007/978-3-031-92196-4_4",
url="https://doi.org/10.1007/978-3-031-92196-4_4"
}