Afgelopen februari dienden onderzoekers van het Centrum Wiskunde & Informatica een bugreport in voor Java. Het standaard sorteeralgoritme, Timsort, bleek in specifieke gevallen te kunnen crashen. De fout kwam aan het licht toen ze het algoritme met formele methoden doorlichtten. Frank de Boer en Stijn de Gouw van het CWI leggen de kwestie uit.
Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
Software (theme 1)
Bits&Chips
Engineering Virtualized Services
Computer Security

de Gouw, C.P.T, & de Boer, F.S. (2015). Formele methoden leggen fout in Java's sorteeralgoritme bloot. Bits&Chips.