有没有人接触过这个工具 SPIN 的模型检查，甚至更多 model checking 的任何信息(并发程序)
最佳答案
是的，SPIN 是一个非常好的模型检查器，但我想知道你想要什么？你只是想听到是的，我听说过并玩过 SPIN 还是你想要关于如何建模检查源代码的建议？
例如，如果您是一名 C 程序员，请使用 ESBMC 编写一个小程序并在其上运行 ESBMC。
这应该让您开始了解可以做什么以及如何做。顺便说一下，对于初学者来说，模型检查不是静态分析。它实际上要强大得多。这是抗静电分析。模型检查实际上“在(非常狭隘的)意义上”模拟您的程序并找到它实际上会失败的情况(参数组合、异常情况、边界情况)。
关于model-checking - 自旋 - 正式验证，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/6038349/