Verification of program computations
Verification of program computations
复制标题
程序计算的验证
DOI：
10.22028/d291-26618
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
C. Rizkallah
中科院分区：
文献类型：
--
作者：
C. Rizkallah
复杂算法的形式化验证具有挑战性。使用当前的验证工具在合理的时间内验证它们的实现是不可行的，并且通常涉及复杂的数学定理。除了每个输出之外，认证算法还计算一个证明输出正确的见证。这种见证人的检查器通常比原始算法简单得多，但它是用户必须信任的全部。检查器的验证在当前工具中是可行的，并且导致可以完全信任的计算。我们描述了一个框架来无缝地验证认证计算。我们通过展示工业级和广泛的算法库LEDA的典型示例的验证来证明我们方法的有效性。我们提出并比较了验证检查器的C实现的两种替代方法。此外，我们还介绍了在NICTA（澳大利亚信息和通信技术卓越研究中心）实习期间所做的工作。这项工作有助于建立一个可行的框架来验证有效的文件系统代码。与我们在本文中解决的算法问题相反，文件系统代码大多是直接的，因此是自动化的良好候选。
Formal verification of complex algorithms is challenging. Verifying their implementations in reasonable time is infeasible using current verification tools and usually involves intricate 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. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA. We present and compare two alternative methods for verifying the C implementation of the checkers. Moreover, we present work that was done during an internship at NICTA, Australia’s Information and Communications Technology Research Centre of Excellence. This work contributes to building a feasible framework for verifying efficient file systems code. As opposed to the algorithmic problems we address in this thesis, file systems code is mostly straightforward and hence a good candidate for automation.
DOI：
10.1007/s10817-013-9289-2
发表时间：
2014
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
E. Alkassar;S. Böhme;K. Mehlhorn;C. Rizkallah
通讯作者：
C. Rizkallah