一句话：提出 TVPI-FP 浮点抽象域，用区间算术重设计算子，高效分析含分支、循环与初等函数的浮点程序。
浮点算术由硬件原生支持，是科学工程数值软件的首选，但由于舍入误差以及 log、arctan、sqrt 等初等函数的频繁使用，此类程序极难分析。本文提出两变量每不等式浮点域（TVPI-FP），一种面向浮点程序分析的、基于数值与约束的抽象域。TVPI-FP 支持真实浮点程序的条件分支、循环与初等函数等全部特征，并在渐近复杂度和实际效率上都很高效，从而克服了先前工具常局限于直线程序或依赖昂贵求解器的不足。其核心思想是在不等式中一致地使用区间算术，并据此重新设计所有算子。大量实验表明，TVPI-FP 常比表达力更强的工具快几个数量级，同时精度相当或更优，并且对含循环与条件分支的现实程序提供更广泛的支持。
Floating-point arithmetic is natively supported in hardware and the preferred choice when implementing numerical software in scientific or engineering applications. However, such programs are notoriously hard to analyze due to round-off errors and the frequent use of elementary functions such as log, arctan, or sqrt. In this work, we present the Two Variables per Inequality Floating-Point (TVPI-FP) domain, a numerical and constraint-based abstract domain designed for the analysis of floating-point programs. TVPI-FP supports all features of real-world floating-point programs including conditional branches, loops, and elementary functions and it is efficient asymptotically and in practice. Thus it overcomes limitations of prior tools that often are restricted to straight-line programs or require the use of expensive solvers. The key idea is the consistent use of interval arithmetic in inequalities and an associated redesign of all operators. Our extensive experiments show that TVPI-FP is often orders of magnitudes faster than more expressive tools at competitive, or better precision while also providing broader support for realistic programs with loops and conditionals.
@article{RiveraFP24,
title = {Floating-Point TVPI Abstract Domain},
author = {Joao Rivera and Franz Franchetti and Markus Püschel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656395}
}