@incollection{BeckertKlebanovSchlager07,
   author        = {Bernhard Beckert and Vladimir Klebanov and Steffen Schlager},
   title         = {Dynamic Logic},
   chapter       = {3},
   part          = {I: Foundations},
   pages         = {69--175},
   editor        = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   booktitle     = {Verification of Object-Oriented Software: The {\KeY} Approach},
   year          = {2007}, 
   series        = {LNCS 4334},
   publisher     = {Springer-Verlag},
   doi           = {10.1007/978-3-540-69061-0_3},
   abstract      = {In the previous chapter, we have introduced a variant of
                    classical predicate logic that has a rich type system and
                    a sequent calculus for that logic. This predicate logic
                    can easily be used to describe and reason about data
                    structures, the relations between objects, the values of
                    variables—in short: about the states of (Java) programs.
                    \newline
                    Now, we extend the logic and the calculus such that we
                    can describe and reason about the behaviour of programs,
                    which requires to consider not just one but several
                    program states.
                    \newline
                    As a trivial example, consider the Java statement
                    x++;. We want to be able to express that this
                    statement, when started in a state where x is zero, terminates in 
                    a state where x is one.}
}