@incollection{BeckertKlebanovWeiss2016, author = {Bernhard Beckert and Vladimir Klebanov and Benjamin Wei{\ss}}, title = {{D}ynamic {L}ogic for {J}ava}, booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice}, publisher = {Springer}, series = {LNCS 10001}, pages = {49--106}, chapter = {3}, part = {I: Foundations}, url = {http://dx.doi.org/10.1007/978-3-319-49812-6_3}, doi = {10.1007/978-3-319-49812-6_3}, year = {2016}, month = dec, abstract = {In this chapter, we introduce an instance of dynamic logic, called JavaDL, that allows us to reason about Java programs. Dynamic logic extends first-order logic and makes it possible to consider several program states in a single formula. Its principle is the formulation of assertions about program behavior by integrating programs and formulas within a single language. We present a sequent calculus for JavaDL, which is used in the {\KeY} System for verifying Java programs. Deduction in this calculus is based on symbolic program execution and simple program transformations and is, thus, close to a programmer's understanding of Java. Besides rules for symbolic execution, the calculus contains rules for program abstraction and modularization, including invariant rules for reasoning about loops and rules that replace a method invocation by the method's contract.} }