使用Bernstein展开和稀疏的Krivine-Stengle表示证明舍入误差边界的认证
摘要：嵌入式系统实现中的浮点误差是不可避免的缺点。计算严格的舍入误差上界对于验证关键软件是绝对必要的。当处理非线性程序时，这个问题变得更加具有挑战性。在本文中，我们提出并比较了基于伯恩斯坦展开和稀疏克里文-斯坦格尔表示的两种新方法，这些方法从全局优化领域中适应了多项式函数实现的舍入误差上界的计算。我们发布了两个相关的软件包FPBern和FPKiSten，并将它们与最先进的工具进行了比较。我们表明，这两种方法在计算准确的上界的同时，实现了竞争性的性能。
作者：Alexandre Rocca and Victor Magron and Thao Dang
论文ID：1610.07038
分类：Numerical Analysis
分类简称：cs.NA
提交时间：2018-02-12