Functional verification with mechanical proofs of TimSort [pdf]

envisage-project.eu

10 pointsjgrodziski1 comment

Key result: there's a bug in Java's library sort. It takes a sort of 6710886 chosen elements to force it, which will force a subscript out of range.