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.
Additional Metadata
ACM Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)
THEME Software (theme 1)
Journal Bits&Chips
Project Engineering Virtualized Services
Citation
de Gouw, C.P.T, & de Boer, F.S. (2015). Formele methoden leggen fout in Java's sorteeralgoritme bloot. Bits&Chips.