浮点运行时间错误检测的关系抽象域
Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors
摘要：
我们提出了一个新的想法，以适应关系抽象域的IEEE 754兼容的浮点数的分析，以静态检测，通过抽象的基于解释的静态分析，潜在的浮点运行时间异常，如溢出或无效操作。为了考虑舍入的非线性，表达式被建模为具有区间系数的线性形式。我们将展示如何扩展现有的数值抽象域，如八角形抽象域，有效地抽象的传递函数的基础上的区间线性形式。我们讨论了具体的不动点稳定技术，并给出了一些实验结果。
英文摘要：
We present a new idea to adapt relational abstract domains to the analysis of IEEE 754-compliant floating-point numbers in order to statically detect, through abstract Interpretation-based static analyses, potential floating-point run-time exceptions such as overflows or invalid operations. In order to take the non-linearity of rounding into account, expressions are modeled as linear forms with interval coefficients. We show how to extend already existing numerical abstract domains, such as the octagon abstract domain, to efficiently abstract transfer functions based on interval linear forms. We discuss specific fixpoint stabilization techniques and give some experimental results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
