On Sunday, December 6, 2015 at 11:43:02 PM UTC+2, leuschel wrote:
Do you have a TLA+ spec of the flawed sorting algorithm ?
No, but the algorithm, as well as a formal specification of the broken assumed invariants and an account of the bug and its discovery, can all be found
here.
I am also not sure what kind of symbolic execution you are after.
The answer of Leslie Lamport refers to BDD-based symbolic model checking.
I am not too sure either (as I am not well-versed in the taxonomy of formal methods), but the kind of symbolic execution used in
KeY :) I believe it is not the same as BDD model-checking.
A tool that is able to automatically check sorting algorithms is a very powerful one to have in your toolbelt, as sorting algorithms -- like state machines -- are exemplars of a very large class of algorithms and data structures (heaps, B-trees and many other kinds of trees, other indexes in general), and if you can check them, you can probably check many interesting programs.
Ron