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

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”

Report about the 1st International HacKeYthon 2018

Two weeks ago, at the 6th and 7th of December, 2018, the 1st International HacKeYthon took place in the rooms of the KIT in Karlsruhe, Germany. In five groups consisting of 3 to 4 participants each we worked on small projects contributing to the overall good of the KeY system. The projects were addressing properties such as usability and performance of the system which are frequently ignored or postponed since their direct value for research is limited.

Continue reading “Report about the 1st International HacKeYthon 2018”