Wednesday, January 18 2017
Showing that Android's, Java's and Python's sorting algorithm is broken, and formally proving the fix
Tim Peters developed the
Timsort hybrid sorting algorithm
in 2002. It is a clever combination of ideas from merge sort and insertion sort, and designed to perform well on real world data. TimSort was first developed for Python, but later ported to Java (where it appears as java.util.Collections.sort and java.util.Arrays.sort) by
(the designer of Java Collections who also pointed out that
most binary search algorithms were broken
). TimSort is today used as the default sorting algorithm for Android SDK, Sun’s JDK and OpenJDK. Given the popularity of these platforms this means that the number of computers, cloud services and mobile phones that use TimSort for sorting is well into the billions.
Fast forward to 2015. After we had successfully verified Counting and Radix sort implementations in Java (
J. Autom. Reasoning 53(2), 129-139
) with a formal verification tool called
, we were looking for a new challenge. TimSort seemed to fit the bill, as it is rather complex and widely used. Unfortunately, we weren’t able to prove its correctness. A closer analysis showed that this was, quite simply, because TimSort was broken and our theoretical considerations finally led us to a path towards finding the bug (interestingly, that bug appears already in the Python implementation). In this presentation, we show how we did it.
Colloquium coordinators are Prof.dr. M. Aiello (e-mail :
Prof.dr. M. Biehl (e-mail:
Effective immediately, UG-authors are entitled to a discount when publishing open access in one of the 271 journals from publisher MDPI. Corresponding authors from the UG will receive a 10% discount on the article processing charge. The only...
This year, the University of Groningen has submitted four research projects to compete for the national Klokhuis Science Prize. The aim of this prize is to introduce a young and wide audience to academic research. The winning project will be...
Non-executive directors (hereafter: directors) have to take a critical stance towards the top managers they supervise. This has been the dominant perspective among researchers and the media after the financial crisis of 2008 and recent major...