Program Analysis for Reliable Numerical Software

CCF-0702622程序分析可靠的数值软件振东SuMany软件系统涉及数值计算，这些系统中的数值错误可能是灾难性的。众所周知的例子包括火星气候轨道器的损失(由于测量单位的误用)和阿丽亚娜5号火箭的爆炸(由于溢出)。研究表明，即使在经过良好测试的代码中，这种错误也经常发生，因为测试数值软件很困难，而且几乎没有静态工具来帮助检测此类错误。该项目旨在开发实用的程序分析技术和工具，以帮助避免常见的数值错误。它主要集中在三个方面：(1)自动尺寸分析和单元检查；(2)静态检测未捕获的异常，如上溢和下溢；(3)误差传播和数值稳定性的静态估计。一般的方法是通过对IEEE浮点标准的形式语义进行建模，并使用适当的约束形式设计近似抽象语义，将这些问题转化为基于约束的程序分析。为了广泛传播研究结果，项目中开发的分析工具将被分发到公共领域，用于教学、研究和实验评估。

CCF-0702622 Program Analysis for Reliable Numerical SoftwareZhendong SuMany software systems involve numerical computation, and numerical errors in these systems can be disastrous. Well-known examples include the loss of the Mars Climate Orbiter (due to a misuse of measurement units) and the explosion of the Ariane 5 rocket (due to an overflow). Studies show that such errors often occur, even in well-tested code, because it is difficult to test numerical software and few static tools exist to help detect such kinds of errors.This project aims at developing practical program analysis techniques and tools to help avoid common classes of numerical errors. It focuses on three main aspects of the problem: (1) automatic dimensional analysis and unit checking, (2) static detection of uncaught exceptions such as overflows and underflows, and (3) static estimation of error propagation and numerical stability. The general approach is to cast these problems as constraint-based program analyses by modeling the formal semantics of the IEEE floating-point standards and designing approximate abstract semantics with appropriate constraint formalisms. For wide dissemination of the research results, analysis tools developed in the project will be distributed to the public domain for use in teaching, research, and experimental evaluation.