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

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



There have been a few research project to verifying C and Java bytecode with TLA+, and there are, of course, quite a few model checkers for C (e.g. CPAChecker), but all approaches and all tools suffer from the same fundamental problem: we are limited in the scale of specification we can verify against arbitrary properties. We can either verify, say, 3000 lines of code or 3000 lines of a high-level spec representing a 100KLOC program, but we can't directly verify large programs (except for very simple, local properties, as sound static analyzers or type systems do). I think that, at least as far as mainstream software goes, people have found that there is more value in verifying high-level specs of large programs vs. verifying very small programs.

For low-level code, you can look at the C2TLA work mentioned above, or, for something less research-grade, see this talk about using TLA+ to specify concurrent algorithms in the Linux kernel.

- Ron

On Saturday, December 7, 2019 at 11:41:22 PM UTC, imran...@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/ed675566-59be-4a55-acc9-878adeb0b66f%40googlegroups.com.