有没有针对 C 程序的静态不变性发现工具？
我正在寻找一种可以静态发现 C 程序中的不变量的工具。我查看了 Daikon 但它只能动态发现不变量。
有没有适合我正在寻找的工具？谢谢！
I'm looking for a tool that can statically discover invariants in C programs. I checked out Daikon but it discovers invariants only dynamically.
Is there a tool available for what I'm looking for? Thanks!
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
如果您指的是最广泛意义上的“不变量”，就像 Daikon 的链接页面所使用的那样，那么许多静态分析工具的工作可以被描述为“发现不变量”，只是可能不是您正在寻找的表达不变量。
Frama-C 的价值分析会累积其结果，即每个语句的所有变量的可能值。在分析结束时，它可以在每个语句处提供有关程序中每个变量的域变化的非关系信息。在此屏幕截图中，一个不变量是
S始终为0, 1 、 3 或 6 就在所选指令之前，用于该确定性程序的所有执行。您问题中的两个隐藏参数是您感兴趣的不变量的形状，以及您想要查找这些不变量的程序的形状。例如，Ira 的回答中提到的 SLAM 旨在处理设备驱动程序代码，并推断仅包含验证系统 API 正确使用所需信息的不变量。另一个工具 Astrée 因在推断正确的不变量来演示运行时方面做得非常出色而闻名飞行控制软件的安全性。
这两个自由度构成了非常大的设计空间。您不会找到适用于所有类型的 C 程序并推断出您可能感兴趣的所有不变量的任何内容，但如果针对特定应用程序领域和类型的不变量细化您的问题，您将有更好的机会找到相关答案。
If you mean "invariant" in the widest sense, as the linked page to Daikon is using, then the work of many static analysis tools can be described as "discovering invariants", just perhaps not the expressive invariants you were looking for.
Frama-C's value analysis accumulates its results, the possible values of all variables, for each statement. At the end of the analysis, it can thus present non-relational information about the domain variation of each variable in the program, at each statement. In this screenshot, an invariant is that
Sis always 0, 1, 3 or 6 just before the selected instruction, for all executions of this deterministic program.The two hidden parameters in your question are the shape of the invariants you are interested in, and the shape of the programs you want to find these invariants for. For instance, SLAM, mentioned in Ira's answer, was designed to work on device driver code, and to infer invariants that just contain the necessary information for verifying proper use of system APIs. Another tool, Astrée, is famous for doing a very good job at inferring just the right invariants to demonstrate runtime safety of flight control software.
The two degrees of freedom make for a very large design space. You won't find anything that works for all kinds of C programs and infers all the invariants you might be interested in, but if you refine your question for specific application domains and kinds of invariants, you will have better chances to find relevant answers.
请参阅SLAM 项目：通过静态分析调试系统软件。它声称可以静态地推断不变量，这正是您所要求的 C 语言。作者汤姆·鲍尔 (Tom Ball) 因其在程序分析方面的出色工作而闻名。
See The SLAM project: debugging system software via static analysis. It claims to infer invariants statically, for just what you asked for, the C language. The author, Tom Ball, is widely known for stellar work in program analysis.