Dynamic Logic for Java

@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.}
}