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”Posts
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.
KeY’s SED Successfully Applied in an Industrial Setting
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”Best Paper Award: “Inferring Secrets by Guided Experiments”
The paper “Inferring Secrets by Guided Experiments” (preprint) from Quoc Huy Do, Richard Bubel and Reiner Hähnle won the Best Paper Award at ICTAC 2017.
Continue reading “Best Paper Award: “Inferring Secrets by Guided Experiments””
16th KeY Symposium 2017
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