提升数值抽象域精度的符号方法
编程语言
2016-08-14 v2
摘要
我们提出了轻量级且通用的符号方法，以提高基于抽象解释的数值静态分析的精度。其主要思想是在将数值表达式输入抽象转换函数之前对其进行简化。一个重要的创新点在于，这些简化是利用分析器动态收集的信息即时执行的。第一种方法称为“线性化”，允许在简化的同时将任意表达式抽象为带有区间系数的仿射形式。第二种方法称为“符号常量传播”，通过以符号方式传播赋值表达式来增强线性化的简化功能。这些方法结合使用，提高了数值抽象域的关系化程度，并使其对程序变换更具鲁棒性。我们展示了如何将它们集成到经典的区间域、八边形域和多面体域中。这些方法已被并入 Astrée 静态分析器中，该分析器用于检查嵌入式关键航空软件中是否存在运行时错误。我们给出了证明其有用性的实验证据。
引用
@article{arxiv.cs/0703076,
title = {Symbolic Methods to Enhance the Precision of Numerical Abstract Domains},
author = {Antoine Miné},
journal= {arXiv preprint arXiv:cs/0703076},
year = {2016}
}
备注
(update: reversed author first and last names)