已收录 272606 条政策
 政策提纲
  • 暂无提纲
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
[摘要] This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.
[发布日期] 2018-01-08 [发布机构] 
[效力级别]  [学科分类] 数值分析
[关键词] ERROR ANALYSIS;FLOATING POINT ARITHMETIC;PROGRAM VERIFICATION (COMPUTERS);PROVING;SEMANTICS;ARITHMETIC;BOOLEAN FUNCTIONS;CONVERGENCE;RECURSIVE FUNCTIONS [时效性] 
   浏览次数:15      统一登录查看全文      激活码登录查看全文