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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Mon, 7 Dec 2015 13:19:24 +0100*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> <91ae46d4-9318-43b6-ac78-2f4ef819011b@googlegroups.com>

Let's just try to be clear about terminology: KeY is an interactive theorem prover that includes an expansion strategy based on symbolic execution (typically, for unfolding a recursive call of a method). The user experience of writing proofs in KeY is closer to writing a TLA+ proof using TLAPS than calling a model checker or constraint solver, which are fully automatic. In particular, KeY requires inductive invariants, and can prove correctness for arbitrary instances. Regards, Stephan |

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

**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

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

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