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

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 2.8

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. 

You can try it out here

We thank all contributors for reaching this milestone.

Nice holidays and a happy new year! 
The KeY Team