您可能对这篇文章感兴趣“<a href="http://www.di.ens.fr/~mine/publi/article-mine-LMCS12.pdf" rel="nofollow">运行时的静态分析嵌入式实时并行 C 程序中的错误”。
Frama-C插件mthread是同时独立开发的。它适用于类似的原则。
上述两种工具中的每一种都是在已经代表至少十人年工作的现有基础上进行的人年工作。正如一些人已经评论过的那样，如果您想为中等规模的程序做任何重要且有用的事情，而您不能仅仅通过阅读来说服自己它是正确的，那么您将需要做很多工作。