[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ logic

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.