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.
Posts
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.
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.
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 “Norwegian Governmental Election Software Formally Verified with KeY”
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”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!
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 “18th KeY Symposium 2019”
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 “Report about the 1st International HacKeYthon 2018”First HacKeYthon taking place in 2018
This year, a new kind of KeY-related event will take place for the very first time, as discussed during the KeY Symposiums in Rastatt and Gothenburg: The HacKeYthon.
Continue reading “First HacKeYthon taking place in 2018”
17th KeY Symposium 2018
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.
Subscribe to our our RSS feed