Program Analysis for Reliable Numerical Software

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