关键词: 浮点程序, 静态分析, 抽象解释, 区间幂集

Abstract: The value range of floating-point variables in the program is very important for analyzing properties and finding run-time errors in floating-point programs. The inexactness of floating-point computation makes it challenging to analyze value range of floating-point variables. The theory of abstract interpretation provides a general framework to analyze the value range of program variables. Under this framework, this paper proposes a new numerical abstract domain, namely powerset of intervals abstract domain, which uses disjunctions of finite numbers of intervals to express the value range of a variable. It is more expressive than the classic interval abstract domain, and can infer some non-convex properties that are beyond the ability of most numerical abstract domains. On this basis, this paper gives a sound floating-point implementation for the new domain, and shows how to analyze floating-point programs soundly using this domain. Finally, this paper implements a static analyzer prototype for analyzing floating-point C programs based on the abstract interpretation framework, which makes use of the floating-point implementation of the powerset of intervals abstract domain to analyze floating-point programs.

Key words: floating-point program, static analysis, abstract interpretation, powerset of intervals