Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis
Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis
复制标题
通过静态分析自动估计已验证的浮点舍入误差
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
C. Muñoz
中科院分区：
文献类型：
--
作者：
Mariano M. Moscato;Laura Titolo;Aaron Dutle;C. Muñoz
本文介绍了一种用于计算浮点功能表达式正式验证的圆形误差界的静态分析技术。该技术基于一种表示的语义，该语义计算浮点圆形错误的象征性估计以及确保其正确性的证明证书。可以使用严格的外壳方法在混凝土输入上评估符号估计，以产生正式验证的数值误差界。所提出的技术在原型研究工具PRECISA（通过静态分析的程序圆形错误认证符）中实施，并用于验证NASA感兴趣的浮点程序。
This paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-off errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-off Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.