程序验证中IEEE 754浮点算术的正确近似
摘要：使用浮点运算验证程序存在一些挑战。关于这类程序推理的困难之一是由于浮点算术的特殊性：舍入误差、无穷大、非数字对象（NaN）、有符号零、非规格化数、不同的舍入模式等。有一个可能的方法是通过一组三元约束（形式为z = x op y）来对计算路径进行建模，并使用约束传播技术推断出变量可能值的新信息。在这种情况下，我们定义并证明了一种算法，用来从已知的另外两个变量的边界开始，精确地限制变量x、y或z的值。对于每个操作和IEEE 754二进制浮点标准定义的每个舍入模式，我们都这样做，即使舍入模式只部分可知。这是首次定义这种所谓的过滤算法，并对其正确性进行形式化证明。这为推进使用浮点运算的程序的形式化验证铺平了道路。
作者：Roberto Bagnara, Abramo Bagnara, Fabio Biselli, Michele Chiari, Roberta Gori
论文ID：1903.06119
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-06-23