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:
http://www.cwi.nl/news/2015/java-bug-fixed-formal-methods-cwi

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
Save
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
Analytics
Tools used to analyze the data to measure the effectiveness of a website and to understand how it works.
Google Analytics
Accept
Decline
Marketing
Set of techniques which have for object the commercial strategy and in particular the market study.
DoubleClick/Google Marketing
Accept
Decline