寻找一本衍生和构建模型检查应用程序的书

Question

我正在自学课程验证，目前正在学习 证明助手. 。我有书 实用逻辑和自动推理手册 这给出了理解这种系统所必需的证据，但对我来说更重要的是，它也使必要算法的实现为 OCAML来源.

我知道在 Wikipedia：模型检查工具 和 Yahoda：验证工具数据库 是开源的，但是当理论，证明，算法和源代码同时提出相互加强时，我也更喜欢它。

有这样的模型检查书吗？

编辑

我可能找到了我想要的东西 计算机科学的数学逻辑 和 Prolog Source. 。由于我没有这本书，有人知道这本书是否符合要求？

Answer 1

约翰·哈里森（John Harrison）的书是从理论到实践并使所有源代码可用的一个例外。我认为您会发现很难找到一本同等的模型检查书，但是有一些可以实现接近近似值。

• 模型检查原理 由Baier和Katoen撰写了许多示例和非常详细的算法描述。
• 旋转模型检查器 杰拉德·霍尔茨曼（Gerard Holzmann）的作者与最早的模型检查员之一的作者有很大不同的待遇。他维护了大约30年的工具，并采用了“程序化”方法。

一个更好的选择可能是遵循在线提供的一些课程的课程注释和实验室分配。至少您会发现理论，实践和示例，即使它们没有在书中组织。

• 埃德蒙·克拉克（Edmund Clarke）在CMU的课程 有一个阅读列表，其中包括一些不同型号检查器的教程。
• Joost-Pieter Katoen的软件验证课程 和后续 实用的模型检查 和 高级模型检查 覆盖很多地面。

最后，这并不是您所要求的，但是由于您一直在研究逻辑和现在的模型检查，因此您将不断地参考抽象解释，这是静态程序分析的基础，并与模型检查密切相关（尽管在模型检查文献中，此连接并不总是明确的）。

• 帕特里克·科索特（Patrick Cousot）的麻省理工学院课程 是一场巡回演出的力量，涵盖了从晶格理论基础到完整实施简单语言的静态分析仪的所有内容。他的课程材料包括所有代码和练习。