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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Mon, 7 Dec 2015 02:23:57 -0800 (PST)*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com> <02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com> <708CF982-1782-422F-8445-6C87C4E7D8D6@gmail.com> <57658c49-b05f-47df-9a41-df4992c873bc@googlegroups.com> <5f44d273-19c0-4086-973c-bbb620e7777b@googlegroups.com> <4ff7ce2d-b955-4953-b58b-8221b6594313@googlegroups.com> <60953B6B-6BF3-478F-BAA2-1EE39514B126@cs.uni-duesseldorf.de>

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

**Follow-Ups**:**Re: [tlaplus] TLA+ logic***From:*Michael Leuschel

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**References**:**TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*Leslie Lamport

**Re: [tlaplus] TLA+ logic***From:*Chris Newcombe

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Michael Leuschel

- Prev by Date:
**Re: Recursive definitions of higher-order operators** - Next by Date:
**Re: [tlaplus] Some distributed TLC errors not displayed in TLA+ Toolbox** - Previous by thread:
**Re: [tlaplus] TLA+ logic** - Next by thread:
**Re: [tlaplus] TLA+ logic** - Index(es):