Formal verification

In 2015, Dutch and German researchers in the EU FP7 ENVISAGE project found a bug in the standard implementation of Timsort. It was fixed in 2015 in Python, Java, and Android.

Specifically, the invariants on stacked run sizes ensure a tight upper bound on the maximum size of the required stack. The implementation preallocated a stack sufficient to sort 2⁶⁴ bytes of input, and avoided further overflow checks.

However, the guarantee requires the invariants to apply to every group of three

1.Previous
3.Next