@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} }
The Java Verification Tool KeY: A Tutorial
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: | The final publication is available at Springer. |
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.