@incollection{BeckertHaehnleHentschel2016,
  author       = {Bernhard Beckert and Reiner H\"ahnle and Martin
                  Hentschel and Peter H. Schmitt},
  title        = {Formal Verification with {\KeY}: {A} Tutorial},
  booktitle    = {Deductive Software Verification - The {\KeY} Book: From Theory to
                  Practice},
  publisher    = {Springer},
  series       = {LNCS 10001},
  pages        = {541--570},
  chapter      = {16},
  part         = {IV: The {\KeY} System in Action},
  url          = {https://dx.doi.org/10.1007/978-3-319-49812-6_16},
  doi          = {10.1007/978-3-319-49812-6_16},
  year         = {2016},
  month        = dec,
  abstract     = {This chapter gives a systematic tutorial introduction on how
                  to perform formal program verification with the {\KeY} system.
                  It illustrates a number of complications and pitfalls,
                  notably programs with loops, and shows how to deal with them.
                  After working through this tutorial, you should be able to
                  formally verify with {\KeY} the correctness of simple Java
                  programs, such as standard sorting algorithms, gcd, etc.}
}