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.