With a small delay after the 19th KeY Symposium, we are very happy to present the new 2.12 release of KeY.
Hans-Dieter Hiep and Stijn de Gouw received a Google Award on 22nd of June, 2023 for finding an integer overflow bug in the LinkedList implementation of the OpenJDK using the KeY verification system.
We congratulate them to their impressive achievement!
The KeY Symposium brings together researchers interested in KeY and related aspects. We will exchange recent achievements, current ideas, discuss the next steps and milestones of the area, as well as future directions in general. Also the latest developments in the KeY tool are presented and discussed.
For more information follow this link
We are happy to announce, that development of KeY is finally public! Our new home is https://github.com/keyproject/ on Github with many repositories, for example,
The original challenge comes from a real-world situation. There is no particular “trick” needed for the specification and verification; it is rather straightforward. Yet, the required annotations to achieve the specification are not too few – making the example a good opportunity to compare different specification languages. Continue reading “Proving Line Wrapping in KeY, Why3, Dafny and Frama-C”
During the VerifyThis competition 2021, KeY was invited to present itself as a Java verification tool.
It is customary for Verify This that for one tool after a brief introduction into the concepts of the tool, the participants are invited to solve a micro challenge – with a little help from present KeY developers.
The KeYNote series is a virtual workshop where teams from Germany, the Netherlands, Norway and Sweden (in lexicographic order) take part and present recent work which uses or extends the KeY verification system.
After almost 2 years of active development, we present now KeY 2.8 just before the year’s end.
The new KeY version comes with significant improvements on the calculus side, but features also a major overhaul of the user interface.
We thank all contributors for reaching this milestone.
Nice holidays and a happy new year!
The KeY Team
Just in time for the holiday season, the new book has arrived.
The LNCS volume 12345* “Deductive Software Verification: Future Perspectives” contains a collection of articles – reflections on the occasion of 20 years of KeY.