A Framework for the Verification of Certifying Computations
A Framework for the Verification of Certifying Computations
复制标题
计算验证的框架
DOI：
10.1007/s10817-013-9289-2
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
C. Rizkallah
中科院分区：
文献类型：
--
作者：
E. 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 automatic 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 use the automatic verifier VCC for establishing the correctness of the checker and the interactive theorem prover Isabelle/HOL for high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA.
登录
查看更多内容
迈向 C0 编译器的形式验证：代码生成和实现正确性
影响因子：
2.8
作者：
Dirk Leinenbach;W. Paul;Elena Petrova
通讯作者：
Elena Petrova
Isabelle/HOL 中顺序命令程序的验证环境
DOI：
10.1007/978-3-540-32275-7_26
发表时间：
2005
期刊：
Comput. Sci. Rev.
影响因子：
--
作者：
Norbert Schirmer
通讯作者：
Norbert Schirmer
DOI：
10.1109/iceccs.2012.27
发表时间：
2012-07
期刊：
2012 IEEE 17th International Conference on Engineering of Complex Computer Systems
影响因子：
--
作者：
Jianqi Shi;J. He;Huibiao Zhu;Huixing Fang;Yanhong Huang;Xiaoxian Zhang
通讯作者：
Jianqi Shi;J. He;Huibiao Zhu;Huixing Fang;Yanhong Huang;Xiaoxian Zhang
通过经过验证的 SAT 验证检查获得工业强度认证的 SAT 解决方案
DOI：
10.1007/978-3-642-14808-8_18
发表时间：
2010
期刊：
IEEE Trans. Computers
影响因子：
--
作者：
A. Darbari;B. Fischer;Joao Marques
通讯作者：
Joao Marques
DOI：
10.1007/978-3-642-22110-1_7
发表时间：
2011
期刊：
Commun. ACM
影响因子：
--
作者：
Eyad Alkassar;S. Böhme;K. Mehlhorn;C. Rizkallah
通讯作者：
C. Rizkallah