伊莎贝尔/霍尔的实际应用实例

Question

我研究了Isabelle教程，它提供了一个示例，说明了它在验证安全协议中的作用。然而，这是有点超出我的理解，因为我只知道基础。我正在寻找一些例子，它们不仅是简单的定理，而且是使用Isabelle/HOL的实际应用。例如，证明一些算法或可能是验证性质系统或一些非平凡的数学定理。在任何地方都有这样的例子吗？

我已经查看了伊莎贝尔官方页面中提供的所有应用程序的列表，但其中大多数都是定理的证明。

我也在看一个使用合金进行文件系统验证的例子。它提供了一个可以验证文件/目录属性的证据。我在找类似的东西。

Answer 1

我现在能想到的几个非常重要的例子是：

• seL4，用C编写的整个操作系统内核，并经过了伊莎贝尔的验证。
• 据我所知，法新社条目线程包含一个完全形式化的字节码编译器，用于一种具有数组和线程的类Java语言。
• 杰里米·阿维格德对素数定理的证明。
• 开普勒猜想的证明。其中一部分是在伊莎贝尔完成的，然而，大部分是在更基本的定理证明器HOL Light中完成的，它的逻辑类似于Isabelle。

正如Joachim提到的，我相信您可以在法新社中找到更有趣的应用程序。