使用浮点运算符对延迟有限域算术的形式证明
摘要：有关有限域算法正确性的证明可以使用Coq等形式化证明工具进行验证，但这些工具需要用户接受广泛的培训。在有限域上延迟解决三角系统问题涉及到整数和浮点数的运算。本文专注于验证证明义务，即浮点操作没有发生舍入误差。我们使用了一个名为Gappa的工具，可以在几分钟内学会使用，生成与浮点算术相关的证明，并隐藏形式化证明工具的技术细节。我们发现现有工具缺少三个功能。第一个是能够在Gappa中使用新引理，这些引理不能轻易表达为重写规则。第二个功能被我们称为“变量交换”，因为它被用于验证循环交换。第三个功能处理大规模循环展开和参数实例化，通过为大量情况生成执行跟踪来实现。我们希望未来这些功能能够被集成到主流的代码验证中。
作者：Sylvie Boldo (INRIA Futurs), Marc Daumas (ELIAUS), Pascal Giorgi (LIRMM)
论文ID：cs/0703026
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2008-07-09