The Java Verification Tool KeY: A Tutorial

@InProceedings{KeYTutorial2024,
  author       = {Bernhard Beckert and
                  Richard Bubel and
                  Daniel Drodt and
                  Reiner H{\"{a}}hnle and
                  Florian Lanzinger and
                  Wolfram Pfeifer and
                  Mattias Ulbrich and
                  Alexander Weigl},
  editor       = {Andr{\'{e}} Platzer and
                  {Kristin Yvonne} Rozier and
                  Matteo Pradella and
                  Matteo Rossi},
  title        = {The Java Verification Tool KeY: A Tutorial},
  booktitle    = {26th International Symposium on Formal Methods ({FM} 2024)},
  series       = {Lecture Notes in Computer Science},
  volume       = {14934},
  venue        = {Milan, Italy},
  year         = {2024},
  month        = sep,
  publisher    = {Springer},
  address      = {Cham},
  pages        = {597--623},
  abstract     = {The KeY tool is a state-of-the-art deductive program verifier
                  for the Java language. Its verification engine is based on a
                  sequent calculus for dynamic logic, realizing forward
                  symbolic execution of the target program, whereby all
                  symbolic paths through a program are explored. Method
                  contracts make verification scalable. KeY combines
                  auto-active and fine-grained proof interaction, which is
                  possible both at the level of the verification target and its
                  specification, as well as at the level of proof rules and
                  program logic. This makes KeY well-suited for teaching
                  program verification, but also permits proof debugging at the
                  source code level. The latter made it possible to verify some
                  of the most complex Java code to date. The article provides a
                  self-contained introduction to the working principles and the
                  practical usage of KeY for anyone with basic knowledge in
                  logic and formal methods.},
  isbn         = {978-3-031-71177-0},
  doi          = {10.1007/978-3-031-71177-0_32},
  links        = {springerlink},
  pdf          = {PDF:/lanzinger/pdf/KeYTutorial.pdf}
}