Everyone here is talking about Timsort, but you should also check out the materials they've published about the KeY project, which they used to carry out this v

Everyone here is talking about Timsort, but you should also check out the materials they've published about the KeY project, which they used to carry out this verification. http://www.key-project.org/~key/eclipse/SED/index.html http://www.key-project.org/~key/eclipse/SED/index.html describes their "symbolic execution debugger", which lets you debug any Java code even if you don't know all the inputs (by simply taking the input as a symbolic value). The screencast is very accessible.