@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 = {http://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.}
}
