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
