This is a more generic question, but I had a bit of trouble finding concrete answers on this.You can find a bunch of examples of industry usage of people using TLA+ with TLC to verify their designs, and that's really cool, but it made me wonder; does anyone know of any examples of using the proof system for that? Is this a silly question?
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/52189418-0691-4252-b43d-94a86782676d%40googlegroups.com.
On 12 Sep 2019, at 10:28, Thomas Gebert <thomas...@gmail.com> wrote:
This is a more generic question, but I had a bit of trouble finding concrete answers on this.You can find a bunch of examples of industry usage of people using TLA+ with TLC to verify their designs, and that's really cool, but it made me wonder; does anyone know of any examples of using the proof system for that? Is this a silly question?
I am not aware of any significant use of TLAPS in industry yet, and quite frankly I don't think that it would be usable at this point for proving the correctness of any significant system. One of the problems is that it requires people to state a full inductive invariant. Of course, I'd be more than happy to be convinced of the contrary.
Stephan
On 12 Sep 2019, at 10:28, Thomas Gebert <thomas...@gmail.com> wrote:
This is a more generic question, but I had a bit of trouble finding concrete answers on this.You can find a bunch of examples of industry usage of people using TLA+ with TLC to verify their designs, and that's really cool, but it made me wonder; does anyone know of any examples of using the proof system for that? Is this a silly question?--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.