Using TLAPS for industrial stuff?

[Thomas Gebert]

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? 

[Tristan Slominski]

Russel Mull just (literally Q&A finished right now :D ) gave a "Exposing Design Flaws in Shared-Clock Systems with TLA+" talk at TLA+ Conf that seems to have been TLA+ for industrial stuff. Videos will be available at some point.

On Thu, Sep 12, 2019 at 12:28 PM 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 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.

[Stephan Merz]

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? 

[Ron Pressler]

I would say this is more of a problem with deductive proofs in general -- a cost/benefit ratio that may be at odds with the constraints of most industrial systems -- rather than TLAPS in particular.

On Thursday, September 12, 2019 at 9:23:58 PM UTC+1, Stephan Merz wrote:

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.