Skip to ContentSkip to Navigation
Over onsNieuws en agendaNieuwsberichten

Colloquium Computer Science S. de Gouw

18 januari 2017

Date:                      

Wednesday, January 18 2017

Speaker:

Stijn de Gouw ( Open University and CWI, Amsterdam)

Room:

5161.0253 (Bernoulliborg)

Time:

15.00

Title:

Showing that Android's, Java's and Python's sorting algorithm is broken, and formally proving the fix


Abstract:

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 Joshua Bloch (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 KeY , 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 : M.Aiello@rug.nl ) and

Prof.dr. M. Biehl (e-mail: M.Biehl@rug.nl )

http://www.rug.nl/research/jbi/news/colloquia/computerscience

Laatst gewijzigd:07 juni 2018 10:59

Meer nieuws

  • 21 juni 2018

    Grenzeloos lallen met Martijn Wieling op Lowlands Science

    Het is bekend dat alcoholgebruik spraak negatief beïnvloedt, maar hoe zit dat bij het spreken van een vreemde taal? Onderzoek suggereert dat het effect hier juist positief lijkt te zijn. Onduidelijk is echter wat er in de mond gebeurt. Dr. Martijn Wieling...

  • 08 juni 2018

    Waardedaling woningen in aardbevingsgebied tot 2015 gemiddeld 9,3%

    Woningen in het Groningse aardbevingsgebied zijn tot 2015 gemiddeld 9,3% in waarde gedaald. Dat concluderen promovendus Nicolás Durán en hoogleraar Ruimtelijke Econometrie Paul Elhorst van de Rijksuniversiteit Groningen. Zij analyseerden data van de...

  • 06 juni 2018

    RUG op plek 120 in QS ranking

    De Rijksuniversiteit Groningen (RUG) staat dit jaar op plaats 120 in de QS World Top University Rankings 2019. Afgelopen twee jaar stond de RUG opplaats 113 in deze lijst van bijna 1.000 universiteiten wereldwijd. Op nationale schaal is Groningen dit...