Posts – Page 2 – The KeY Project

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 →

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 →

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.

Continue reading “17th KeY Symposium 2018” →

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 →

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

Continue reading “16th KeY Symposium 2017” →

Proving JDK’s Dual Pivot Quicksort Correct

by Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt and Mattias Ulbrich Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimized implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) implementation of TimSort. We have now formally analysed the other implementation of sorting in the JDK standard library: A highly efficient implementation of a dual pivot quicksort algorithm. We were able to deductively prove that the algorithm implementation is correct. However, a loop invariant which is annotated to the source code does not hold. Continue reading →

New Feature: State Merging in KeY

Current nightly builds of KeY contain a new feature called state merging, a technique to decrease the size of proof trees arising from the symbolic execution of large programs. Continue reading “New Feature: State Merging in KeY” →

How researchers from UPM and IMDEA used KeY as backend

Researchers (Julio Mariño Raúl, N. N. Alborodo, Lars-Åke Fredlund and Ángel Herranz) from UPM and IMDEA (both Madrid, Spain) developed a methodology to synthesize verifiable concurrent Java components from formal models. Continue reading “How researchers from UPM and IMDEA used KeY as backend” →

The new KeY Book has been published

A years long effort comes to a successful conclusion. On December, 20th the new KeY book became available online. Most of the book’s content is new or largely rewritten compared to the first KeY Book.

Go here for more information and supplementary material.

Subscribe to our our RSS feed