Posts

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.

The new version mainly contains improvements under the hood, such as completely rewritten parsers for JML and the internal problem/proof format or better translation of problems to SMT-LIB2.

You can download and try it out here.

We thank all developers and testers for reaching this milestone!

Nice holidays and a happy new year! 
The KeY Team

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

Proving the Correctness of Program Transformations with Abstract Execution and REFINITY

Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores.

Continue reading “Proving the Correctness of Program Transformations with Abstract Execution and REFINITY”