中文摘要：

提出一种抽象解释和有界模型验证的数值型运行时错误分析方法.利用抽象解释方法分析程序数值变量范围,获得每个程序点达到不动点的变量初步值范围信息.根据待分析的运行时错误类型,在相关需要检测的程序点处将数值变量取值信息转化为断言或假设形式插入程序中,将带有断言和假设的程序转化为布尔公式,验证其可满足性,进而验证断言的正确性.实验证明,该方法与现有方法相比,在精度和效率两方面都有良好的表现.

英文摘要：

A novel method of numerical runtime error analysis is presented based on abstract interpretation and bounded model checking. Firstly, the scope of program numeric variables is analyzed with abstract interpretation to obtain the variable range information of each program fixed point. Second, based on runtime error type to be analyzed, the value of the variable information is changed into the form of assertions or assumptions. Then the program is inserted at the detected point. Finally, the program is changed with assertions and assumptions into Boolean formula to verify the satisfiability of Boolean formula, and then to verify the correctness of the assertion. Experiment results show that the method has good performance both in terms of accuracy and efficiency compared with the existing methods.