Using the KeY Prover

@incollection{AhrendtGrebing2016,
  author       = {Wolfgang Ahrendt and Sarah Grebing},
  title        = {Using the {\KeY} Prover},
  booktitle    = {Deductive Software Verification - The KeY Book: From Theory to
                  Practice},
  publisher    = {Springer},
  series       = {LNCS 10001},
  pages        = {495--539},
  chapter      = {15},
  url          = {http://dx.doi.org/10.1007/978-3-319-49812-6_15},
  doi          = {10.1007/978-3-319-49812-6_15},
  year         = {2016},
  month        = dec,
  abstract     = {This chapter is a self-contained introduction into the usage
                  of the KeY prover, a tool for proving formulas of a program
                  logic called Java Dynamic Logic. It does not assume the
                  reader to have read any other chapter of the book in advance.
                  Here, we discuss the usage of the KeY prover in isolation.
                  For a tutorial on the most common context of the prover,
                  i.e., the KeY verification process, we refer to the chapter
                  `Formal Verification with {\KeY}: A Tutorial'. The present
                  chapter takes entirely the user's perspective on the \KeY
                  prover, and the GUI plays an important role. However, we do
                  not only introduce the various ways of using, and interacting
                  with, the \KeY prover. Rather, the various visible artifacts
                  the prover acts on, in particular the logic and the taclet
                  language, are introduced on the side, on demand, and example
                  driven, in a light-weight manner. This chapter is meant to be
                  read with the KeY system up and running, such that every step
                  can be tried out immediately in the system. The concepts that
                  will be introduced along with the usage of the prover include
                  \KeY problem files, propositional, first-order, and dynamic
                  logic, sequent calculus, proof construction, proof navigation
                  and manipulation, taclets, interactive and automated proving,
                  quantifier instantiation, and symbolic execution. Most of
                  these topics are discussed in much greater detail in other
                  chapters within this book, but appear here in the context of
                  using the \KeY prover.}
}