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

[imranmeah91@xxxxxxxxx]

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.