Researchers from the Formal Methods group at CWI fixed a bug in programming language Java in February 2015. They found an error in a broadly applied sorting algorithm, TimSort, which could crash programs and threaten security. The bug had already been known from 2013 but was never correctly resolved. When researcher Stijn de Gouw attempted to prove the correctness of TimSort, he encountered the bug. His bug report with an improved version has now been accepted. This version of TimSort is used by Android.

Java is broadly used because it provides a lot of support in the form of libraries. TimSort is part of the ‘java.util.Arrays’ and ‘java.util.Collections’ libraries. When a bug occurs there, it will appear on many places. Frank de Boer, head of the Formal Methods group says: “So far, it was one of the hardest correctness proofs ever of an existing Java library. It required more than two million rules of inference and thousands of manual steps. With such an important language like Java, it is important that software does not crash. This result illustrates the importance of formal methods for society.” The study was co-funded by the EU project Envisage.

More information:

Next issue: July 2023
Special theme:
"Eplainable AI"
Call for the next issue

Image ERCIM News 101 epub
This issue in ePub format

Get the latest issue to your desktop
RSS Feed
Cookies user preferences
We use cookies to ensure you to get the best experience on our website. If you decline the use of cookies, this website may not function as expected.
Accept all
Decline all
Read more
Tools used to analyze the data to measure the effectiveness of a website and to understand how it works.
Google Analytics
Set of techniques which have for object the commercial strategy and in particular the market study.
DoubleClick/Google Marketing