Verification of Certifying Computations
Verification of Certifying Computations
复制标题
计算证明的验证
DOI：
10.1007/978-3-642-22110-1_7
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
C. Rizkallah
中科院分区：
文献类型：
--
作者：
Eyad Alkassar;S. Böhme;K. Mehlhorn;C. Rizkallah
复杂算法的形式验证是具有挑战性的。验证它们的实现超出了当前验证工具的技术水平，并证明它们的正确性通常涉及到非平凡的数学定理。证明算法除了计算每个输出之外，还计算一个证明输出是正确的见证。这样的证人的检查器通常比原始算法简单得多-但这是用户必须信任的全部。使用当前的工具对检查器进行验证是可行的，并导致完全可信的计算。在本文中，我们开发了一个无缝验证证明计算的框架。自动验证器VCC用于检查代码的正确性，交互式定理证明器Isabelle/HOL针对算法的高级数学性质。通过对算法库LEDA的一个典型例子的验证，证明了该方法的有效性。
Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm - yet it is all the user has to trust. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted. In this paper we develop a framework to seamlessly verify certifying computations. The automatic verifier VCC is used for checking code correctness, and the interactive theorem prover Isabelle/HOL targets high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of a typical example of the algorithmic library LEDA.