Program Analysis for Reliable Numerical Software

CCF-0702622可靠数值软件的程序分析许多软件系统涉及数值计算，这些系统中的数值错误可能是灾难性的。众所周知的例子包括火星气候轨道器的损失（由于测量单位的滥用）和阿丽亚娜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.