使用Gappa认证浮点实现
Certifying floating-point implementations using Gappa
AI总结：
本文介绍使用Gappa证明辅助工具自动验证浮点程序的数值属性，包括值范围与误差界，并通过实际示例展示其高效性与可靠性。
摘要：
对浮点程序的高置信度需要证明最终值和中间值的数值属性。可能需要保证某个值保持在某个范围内，或者相对于某个理想值的误差有良好的界限。这样的工作每行代码可能需要几行证明，并且通常会被代码的最小更改（例如出于维护或优化目的）破坏。因此，手动认证这些程序非常繁琐且容易出错。本文讨论了在此背景下使用Gappa证明辅助工具。Gappa相比以前的方法有两个主要优势：其输入格式非常接近要验证的实际C代码，并且它使用区间算术自动进行误差评估和传播。此外，它可以用于增量地证明与C代码相关的复杂数学属性。然而，它不需要任何关于自动定理证明的具体知识，因此对广大社区是可访问的。此外，Gappa可以生成结果的形式化证明，这些证明可以由像Coq这样的低级证明辅助工具独立检查，从而为数值代码的认证提供更高的置信度。本文通过一个实际大小的示例——一个具有正确舍入输出的基本函数——展示了该工具的使用。
英文摘要：
High confidence in floating-point programs requires proving numerical properties of final and intermediate values. One may need to guarantee that a value stays within some range, or that the error relative to some ideal value is well bounded. Such work may require several lines of proof for each line of code, and will usually be broken by the smallest change to the code (e.g. for maintenance or optimization purpose). Certifying these programs by hand is therefore very tedious and error-prone. This article discusses the use of the Gappa proof assistant in this context. Gappa has two main advantages over previous approaches: Its input format is very close to the actual C code to validate, and it automates error evaluation and propagation using interval arithmetic. Besides, it can be used to incrementally prove complex mathematical properties pertaining to the C code. Yet it does not require any specific knowledge about automatic theorem proving, and thus is accessible to a wide community. Moreover, Gappa may generate a formal proof of the results that can be checked independently by a lower-level proof assistant like Coq, hence providing an even higher confidence in the certification of the numerical code. The article demonstrates the use of this tool on a real-size example, an elementary function with correctly rounded output.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
