The Java Verification Tool KeY: A Tutorial

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich und Alexander Weigl
In:26th International Symposium on Formal Methods (FM 2024)
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:14934
Jahr:2024
Seiten:597-623
PDF:
DOI:10.1007/978-3-031-71177-0_32
Links:

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.

BibTeX

@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}
}