@book{KeYBook2016,
  editor       = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and
                  Reiner H\"ahnle and Peter H. Schmitt and Mattias Ulbrich},
  title        = {Deductive Software Verification - The {\KeY} Book: From Theory
                  to Practice},
  series       = {Lecture Notes in Computer Science},
  volume       = {10001},
  publisher    = {Springer},
  url          = {https://dx.doi.org/10.1007/978-3-319-49812-6},
  doi          = {10.1007/978-3-319-49812-6},
  year         = {2016},
  abstract     = {Static analysis of software with deductive methods is a highly dynamic field
                  of research on the verge of becoming a mainstream technology in software
                  engineering. It consists of a large portfolio of - mostly fully automated -
                  analyses: formal verification, test generation, security analysis,
                  visualization, and debugging. All of them are realized in the state-of-art
                  deductive verification framework {\KeY}.
                  \newline
                  This book is the definitive guide to {\KeY} that lets you explore the full
                  potential of deductive software verification in practice. It contains the
                  complete theory behind {\KeY} for active researchers who want to understand it in
                  depth or use it in their own work. But the book also features fully
                  self-contained chapters on the Java Modeling Language and on Using {\KeY} that
                  require nothing else than familiarity with Java. All other chapters are
                  accessible for graduate students (M.Sc. level and beyond).
                  \newline
                  The {\KeY} framework is free and open software, downloadable from the book
                  companion website which contains also all code examples mentioned in this
                  book.}
}