Posts – Page 3 – The KeY Project

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

Proving JDK’s Dual Pivot Quicksort Correct

New Feature: State Merging in KeY

How researchers from UPM and IMDEA used KeY as backend

The new KeY Book has been published

KeY talk at the British Computer Society

15th KeY Symposium 2016