基础多模态程序验证器

《Proceedings of the ACM on Programming Languages》：Foundational Multi-Modal Program Verifiers

多模态程序验证通过动态和符号技术结合自动化与交互式工具验证代码正确性，需形式化证明工具自身正确性。本文提出基于更高阶逻辑的莫迪克浅嵌入框架，提供支持状态、异常等效应的转换器代数，实现自动化验证条件生成与SMT求解器结合的自动化证明，并通过分布式协议和Dafny风格规格书验证案例。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

多模态程序验证是一种使用动态和符号技术来验证代码是否符合其规范的过程，并通过自动化和交互式机器辅助工具的组合来证明其正确性。为了确保可信度，这些验证工具本身必须具有形式化的正确性证明，以确保在任何根据特定规范进行验证的程序执行时不会违反规范的要求。在具有小型可信核心的通用证明辅助工具中被证明正确的验证工具通常被称为基础性验证工具。

我们提出了一个框架，该框架有助于构建既基础又多模态的程序验证器。我们的方法采用了将可执行程序语义以单子形式嵌入到基于高阶逻辑的定理证明器（在我们的案例中是Lean证明辅助工具）中的著名思想。我们为这种语义提供了一个单子转换器库，编码了各种计算效应，包括状态、发散、异常和非确定性。我们工作的关键理论创新是单子转换器代数，它使得能够自动推导出相应的正确性验证条件生成器。我们展示了使用现成的SMT求解器可以自动证明这些验证条件，并在自动化失败时提供交互式证明模式。为了展示我们框架的多样性，我们将其实例化为两个基础性多模态验证器，用于推理（1）分布式协议的安全性和（2）Dafny风格的命令式程序规范，并用它们来机械地验证了一些非平凡的案例研究。

AI摘要

AI生成的摘要（实验性）

此摘要是使用自动化工具生成的，并非由文章作者编写或审核的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解本文的工作。它旨在补充作者提供的摘要，后者仍然是论文的主要摘要。完整文章仍然是权威版本。点击这里了解更多。

点击这里对摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进和未来重新生成的版本。

要查看此由AI生成的简单语言摘要，您必须具有高级访问权限。