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