Frama-C已经验证了吗？

Question

我很好奇Frama-C是否已经使用Frama-C或其他验证框架进行了正式验证，因为Frama-C中的错误可能会导致Frama-C验证的程序中的错误被忽视。

我知道这个过程会非常繁琐，但考虑到 Frama-C 在各个行业中用于核系统和航空等关键应用，我希望一些组织愿意对其进行验证。

Answer 1

你的问题的第一部分非常容易回答：Frama-C是用OCaml编写的，专门用于验证用C编写的程序，因此你无法在Frama-C中验证Frama-C。

关于通过其他方式验证 Frama-C，已经有各种工作致力于形式化一些分析，但通常仅针对 C 和 ACSL 的子集。这通常包括 Coq 证明助手。此类示例的非详尽列表包括：

• Paolo Herm 的 PhD 关于 Jessie 插件
• Jean-Christophe Léchenet 的 PhD 关于切片插件
• Dara Ly 的 PhD 关于 E-ACSL 插件
• Lionel Blatter 的 文章 关于 RPP 插件（部分是 WP）

最后，关于在具有严格限制的工业领域中的部署（以某些认证机构的形式给予一些正式的——律师意义上的而不是数学上的一印章批准），Airbus和Thales已经发表了关于如何使用它们的论文Frama-C 帮助他们获得了产品认证。