@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",
doi="10.1007/978-3-031-92196-4_4",
url="https://doi.org/10.1007/978-3-031-92196-4_4"
}
The Many Uses of Dynamic Logic
| Author(s): | Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich |
|---|---|
| In: | Go Where the Bugs Are: Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday |
| Publisher: | Springer Nature Switzerland |
| Year: | 2025 |
| Pages: | 56-82 |
| Preprint/PDF: | TheManyUsesOfDL.pdf |
| URL: | https://doi.org/10.1007/978-3-031-92196-4_4 |
| DOI: | 10.1007/978-3-031-92196-4_4 |
| Links: | The final publication is available at Springer. |
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.