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
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.
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”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”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!
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”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”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”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.
The Symbolic Execution Debugger (SED) is a debugging and visualization tool based on KeY’s symbolic execution engine that can be used, just like a standard debugger, without any specialist knowledge. Now, the SED has successfully been applied by Aniket Kulkarni from Tata Consultancy Services in the validation of an industrial software component. He concludes that the “SED tool is useful for applying Symbolic Execution techniques as visual feedback is given to the developer”.
Continue reading “KeY’s SED Successfully Applied in an Industrial Setting”
Subscribe to our our RSS feed