Supported Java FeaturesJava is a very complex language which massively evolved over the time. KeY does not support all Java features. Some of those, like floating-point arithmetic, are in principle hard to handle from a theorem-proving point of view; others, like Generics and Lambdas, could be considered in future versions of the system. The following (incomplete) table gives an overview about the state of selected Java features in the current KeY version. Features shaded in green are supported, those in red are unsupported; features in yellow are in principle not supported, but can be treated with restrictions by a workaround supplied by KeY. A list of supported JML features is available here.
|Basic Java 1.2 features||KeY supports Integer arithmetic (for both mathematical Integers and actual Integer types with overflows), Strings, inheritance, dynamic dispatch, loops, recursion, …|
|Enhanced “for” loops||Supported.|
|Floating point types||Supported, reasoning via axioms and by using SMT solvers with float support.|
|Library methods||KeY will throw an error when you use libraries the code of which is not in KeY’s classpath. However, we have a plugin in our eclipse extension which can create stubs with default contracts for library methods such that you can directly start proving properties about your code, or manually refine the stub specifications before.|
|Generics||Unsupported; However, a tool to statically remove Generics from the code can be downloaded here.|
|try-with-resources and multi-catch (both Java 7)||Unsupported.|
|Java 8 features (lambdas etc.)||Unsupported.|
Video Tutorial: Interactive Verification with the Symbolic Execution Debugger (SED)
Video Tutorial: Proof Attempt Inspection with the Symbolic Execution Debugger
Formal Verification with KeY: A Tutorial (2016)By Bernhard Beckert, Reiner Hähnle, Martin Hentschel and Peter H. Schmitt Book chapter of the KeY book. This chapter gives a systematic tutorial introduction on how to perform formal program verification with the KeY system. It illustrates a number of complications and pitfalls, notably programs with loops, and shows how to deal with them. After working through this tutorial, you should be able to formally verify with KeY the correctness of simple Java programs, such as standard sorting algorithms, gcd, etc. Find this tutorial on SpringerLink
Note: The following tutorials may require older versions of KeY.
Verifying Object-Oriented Programs with KeY: A Tutorial (2007)By Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, and Peter H. Schmitt. Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers. Download this tutorial.
Relevant blog posts
Towards a Usable and Sustainable Deductive Verification Tool Proceedings Article
In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part II, pp. 281–300, Springer, 2022.
Dijkstra's Legacy on Program Verification Book Section
In: Apt, Krzysztof R.; Hoare, Tony (Ed.): Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105–140, ACM / Morgan & Claypool, 2022.
Delta-based verification of software product families Proceedings Article
In: Tilevich, Eli; Roover, Coen De (Ed.): GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17 - 18, 2021, pp. 69–82, ACM, 2021.
Modular, Correct Compilation with Automatic Soundness Proofs Proceedings Article
In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Modeling, pp. 424–447, Springer International Publishing, Cham, 2018, ISSN: 0302-9743.
Verifying OpenJDK's Sort Method for Generic Collections Journal Article
In: Journal of Automated Reasoning, 2017, ISSN: 1573-0670.
A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows Proceedings Article
In: Polikarpova, Nadia; Schneider, Steve (Ed.): Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pp. 279–294, Springer, 2017.
An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier Proceedings Article
In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 403-413, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.
The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Proceedings Article
In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.
Integrating Symbolic Execution, Debugging and Verification PhD Thesis
Technische Universität Darmstadt, 2016.
A General Lattice Model for Merging Symbolic Execution Branches Proceedings Article
In: Ogata, Kazuhiro; Lawford, Mark; Liu, Shaoying (Ed.): Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, pp. 57–73, Springer International Publishing, 2016.