• 学术研究 •

基于浮点区间幂集抽象域的浮点程序分析

1. 国防科学技术大学 计算机学院，长沙 410073
• 出版日期:2013-03-01 发布日期:2013-03-05

Floating-Point Program Analysis Based on Floating-Point Powerset of Intervals Abstract Domain

JIANG Jiahong+, CHEN Liqian, WANG Ji

1. School of Computer, National University of Defense Technology, Changsha 410073, China
• Online:2013-03-01 Published:2013-03-05

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.