我正在寻找一种可以在 C 程序中静态发现不变量的工具。我检查了Daikon，但它只是动态地发现不变量。
是否有适合我正在寻找的工具？谢谢！
问问题
383 次
2 回答
5
请参阅SLAM 项目：通过静态分析调试系统软件。它声称静态推断不变量，正如您所要求的，C 语言。作者 Tom Ball 因其在程序分析方面的出色工作而广为人知。
于 2011-11-11T02:57:29.220 回答
4
如果您指的是最广泛意义上的“不变量”，正如 Daikon 的链接页面所使用的那样，那么许多静态分析工具的工作可以被描述为“发现不变量”，而可能不是您正在寻找的表达不变量。
Frama-C 的值分析为每个语句累积其结果，即所有变量的可能值。因此，在分析结束时，它可以在每个语句处呈现有关程序中每个变量的域变化的非关系信息。在此屏幕截图中，对于此确定性程序的所有执行，不变量S始终是所选指令之前的 0、1、3 或 6。
您问题中的两个隐藏参数是您感兴趣的不变量的形状，以及您要为其查找这些不变量的程序的形状。例如，Ira 的回答中提到的 SLAM 旨在处理设备驱动程序代码，并推断仅包含验证系统 API 正确使用所需信息的不变量。另一个工具Astrée以在推断正确的不变量以证明飞行控制软件的运行时安全性方面做得非常出色而闻名。
两个自由度构成了非常大的设计空间。您不会找到任何适用于所有类型的 C 程序并推断出您可能感兴趣的所有不变量的东西，但是如果您针对特定的应用程序域和不变量类型细化您的问题，您将有更好的机会找到相关的答案。
于 2011-11-11T05:20:31.073 回答