Posts – Page 2 – The KeY Project

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.

Continue reading “KeY Tutorial at VerifyThis 2021” →

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.

Continue reading “KeYNote Series” →

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

The new book has arrived!

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!” →

Norwegian Governmental Election Software Formally Verified with KeY

In his recently finished Master’s thesis, Henrik Torland Klev verified (parts of) EVA, the main support system for elections in municipalities and counties in Norway, using the KeY prover.

Continue reading →

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 Smart Contracts with KeY

With smart contracts, it is really important to get them right at the first try. See how KeY can be used to prove the correctness of Hyperledger Fabric chaincode!

Go to project page

18th KeY Symposium 2019

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.

Continue reading →

Report about the 1st International HacKeYthon 2018

Table of Contents

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 →

Subscribe to our our RSS feed