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,
Continue reading “Towards an open development model for KeY”
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.
Continue reading “The new book has arrived!”
Just in time to put it under your christmas tree, we are happy to present the new 2.10 version of KeY.
You can download and try it out here.
Continue reading “KeY 2.10”
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”
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.
Continue reading “KeY Tutorial at VerifyThis 2021”