Program Analysis for Reliable Numerical Software

可靠数值软件的程序分析

• 批准号: 0702622
• 负责人: Zhendong Su
• 金额: $ 40万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-01 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0702622&HistoricalAwards=false
• 关键词: Program; Analysis; Reliable; Numerical; Software

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.

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