提高数值抽象域精度的符号方法
Symbolic Methods to Enhance the Precision of Numerical Abstract Domains
摘要：
本文提出了一种轻量级的通用符号化方法来提高基于抽象解释的数值静态分析的精度。其主要思想是在将数值表达式转化为抽象传递函数之前对其进行简化。一个重要的新颖之处在于，这些简化是使用分析器动态收集的信息实时执行的。第一种方法称为“线性化”，允许将任意表达式抽象为具有区间系数的仿射形式，同时简化它们。第二种方法，称为“符号常数传播”，通过以符号方式传播指定的表达式来增强线性化的简化特征。结合在一起，这些方法增加了数值抽象域的关系水平，使它们对程序转换更强大。我们展示了如何将它们整合在经典的区间，八角形和多面体域。这些方法已被纳入Astronée静态分析仪中，用于检查嵌入式关键航空电子软件中是否存在运行时错误。我们提出了一个实验证明其实用性。
英文摘要：
We present lightweight and generic symbolic methods to improve the precison of numerical static analyses based on Abstract Interpretation. The main idea is to simplify numerical expressions before they are fed to abstract transfer functions. An important novelty is that these simplifications are performed on-the-fly, using information gathered dynamically by the analyzer. A first method, called "linearization," allows abstracting arbitrary expressions into affine forms with interval coefficients while simplifying them. A second method, called "symbolic constant propagation," enhances the simplification feature of the linearization by propagating assigned expressions in a symbolic way. Combined together, these methods increase the relationality level of numerical abstract domains and make them more robust against program transformations. We show how they can be integrated within the classical interval, octagon and polyhedron domains. These methods have been incorporated within the Astrée static analyzer that checks for the absence of run-time errors in embedded critical avionics software. We present an experimental proof of their usefulness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
