在哪里可以找到更复杂的使用 Hoare 逻辑来验证 Isabelle/HOL 中的程序的示例？
我最近了解了在 Isabelle/HOL 中使用 Hoare 逻辑进行程序验证的这一方面。我发现本教程中的示例是简单的示例（http://www.inf.ed.ac.uk/teaching/courses/ar/HoareLogicLecture.thy）。在哪里可以找到更复杂的使用 Hoare 逻辑来验证 Isabelle/HOL 中的程序的示例？
问问题
88 次
1 回答
1
seL4 证明可能符合要求。例如，整个内核功能规范的不变性保存证明：https ://github.com/NICTA/l4v/blob/master/proof/invariant-abstract/README.md
于 2019-09-02T14:37:46.960 回答