EAGER: Toward Numerically Robust Software

EAGER：迈向数值稳健的软件

• 批准号: 1349528
• 负责人: Zhendong Su
• 金额: $ 30万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2016-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1349528&HistoricalAwards=false
• 关键词: EAGER; Toward; Numerically; Robust; Software

Society increasingly depends on numerical software, which uses finite precision arithmetic to approximate the reals and necessarily introduces approximation and error. Anti-lock breaks and medical devices such as haptic control systems for remote surgery are two such examples. Numerical errors in these systems can be disastrous. Toyota suspects such errors contributed to its recent, costly unintended acceleration problem, and the Ariane 5 rocket exploded due to an overflow in its inertial reference system. This project explores practical techniques to test and analyze numerical software, which will advance the state-of-the-art in engineering robust numerical software to help avoid costly, dangerous errors.In particular, the project focuses on the two most fundamental sources of numerical errors: uncaught exceptions and numerical stability and accuracy. The proposed core framework is centered around symbolic execution, and domain insights will be used to develop principles and heuristics to make it practical. This project will complete several preliminary research tasks to validate and demonstrate the promise of the proposed general approach. It will explore new problem modeling strategies for numerical accuracy and stability, examining realistic numerical constraints to build insights into constraint solving strategies and algorithms, and improving the promising Ariadne symbolic analysis infrastructure.

社会越来越依赖于数值软件，该软件使用有限的精度算术来逼近真实，并且必然会引入近似和误差。抗锁断裂和医疗设备（例如用于远程手术的触觉控制系统）就是两个这样的例子。这些系统中的数值错误可能是灾难性的。 丰田人怀疑这种错误导致了其最近的昂贵的意外加速问题，并且由于其惯性参考系统的溢出而爆炸了Ariane 5火箭。 该项目探讨了测试和分析数值软件的实用技术，这些技术将推进工程鲁棒数值软件的最新技术，以帮助避免昂贵，危险的错误。尤其是，该项目着重于两个最根本的数值错误来源：未熟悉的异常和数值稳定性和数值稳定性和准确性。拟议的核心框架围绕象征性执行，域的见解将用于制定原理和启发式方法以使其实用。该项目将完成几项初步研究任务，以验证和证明拟议的一般方法的希望。它将探索用于数值准确性和稳定性的新问题建模策略，研究现实的数值约束，以建立对解决策略和算法的洞察力，并改善有希望的Ariadne符号分析基础架构。