浮点程序鲁棒性分析的非局部方法
摘要：鲁棒性是一种标准的正确性属性，直观上意味着如果程序的输入变化小于一个固定的小量，那么输出只会发生微小的变化。这个概念在浮点数程序的舍入误差分析中很有用，因为它有助于确定由测量误差和浮点计算引入的输出误差的上限。由于关键结构（如条件语句和while循环）不具备鲁棒性，组合方法通常不起作用。我们提出了一种证明while循环鲁棒性的方法。这种方法是非局部的，因为它不是将分析拆解成单行代码，而是检查其结构的某些全局属性。我们在两个标准算法（CORDIC计算余弦和Dijkstra的最短路径算法）上展示了我们方法的适用性。
作者：Ivan Gazeau (LIX, INRIA Saclay - Ile de France), Dale Miller (LIX, INRIA Saclay - Ile de France), Catuscia Palamidessi (LIX, INRIA Saclay - Ile de France)
论文ID：1202.0693
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-07-10