Re: [tlaplus] Has anyone tried using tla+ and clang for source level model checking?

[Morgan Weetman <morgan.weetman@xxxxxxxxx>]

Hi Imran, 

IANAE..  but I think what you get from simplifying with clang or similar will still be too low level for Tla+. If you have access to source code then it should be pretty straight forward to extract/summarise the logic by hand.

In any case, I'm interested to see how you go so please keep us in the loop,

Thanks 

On Sun., 8 Dec. 2019, 10:41 , <imranmeah91@xxxxxxxxx> wrote:

I understand Tla+ is supposed to be above the code level. I  work mainly with finding issue with existing code base.
What I would do is read the code and abstract away non important part and build model in tla+.

I was wondering if any one has used tool like clang to extract relevant information from code like thread created, mutex and whatnot and try to show absent of any concurrent issue.

I would appreciate if any one has any lead and share their experience in this arena.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/26307f56-a2ef-49a4-bae4-b9db1bcbc396%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKFE_%3DSdfOdee-UjP_C%2B1ZXA1L0op4Mx3Gn5b4LUmUJhRuOuOw%40mail.gmail.com.