The HacKeYthon is a two-day event with the goal of bringing forward the development of the KeY system and to transfer knowledge from experienced developers to newer members and associates of the KeY project.
Continue reading “2nd HacKeYthon 2024”Posts
20th KeY Symposium 2024
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
KeY 2.12
With a small delay after the 19th KeY Symposium, we are very happy to present the new 2.12 release of KeY.
You can download it from GitHub. Continue reading “KeY 2.12”
CWI-Researchers win Google award using 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!
Continue reading “CWI-Researchers win Google award using KeY”
19th KeY Symposium 2023
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
Towards an open development model for KeY
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,
KeY 2.10
Just in time to put it under your christmas tree, we are happy to present the new 2.10 version of KeY.
Proving Line Wrapping in KeY, Why3, Dafny and Frama-C
This is a short comparison report about a verification task solved with KeY, Why3, Dafny and Frama-C.
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”
KeY Tutorial at VerifyThis 2021
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.
KeYNote Series
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.
Subscribe to our our RSS feed