The automation offered by modern program proof tools goes hand in hand with the capability to interact with the tool when the verification fails. The SPARK proof tool tries to help the user by providing the right information, so that the user can help the tool complete the proof. In this article, we present these mechanisms and how they work concretely on a simple running example.
翻译：现代程序验证工具提供的自动化与验证失败时与工具互动的能力同时并进。 SPARK 验证工具试图通过提供正确信息帮助用户,以便用户能够帮助工具完成验证。在本篇文章中,我们用一个简单的运行示例来介绍这些机制及其具体运作方式。
相关内容
Arxiv
0+阅读 · 2021年10月6日
Arxiv
0+阅读 · 2021年10月4日
Arxiv
0+阅读 · 2021年10月4日
Arxiv
0+阅读 · 2021年10月4日
相关VIP内容
相关资讯
相关论文
Arxiv
0+阅读 · 2021年10月6日
Arxiv
0+阅读 · 2021年10月4日
Arxiv
0+阅读 · 2021年10月4日
Arxiv
0+阅读 · 2021年10月4日
微信扫码咨询专知VIP会员