EAGER: Toward Numerically Robust Software

社会越来越依赖于数值软件，它使用有限精度的算法来逼近实数，必然会引入近似和误差。防锁死装置和远程手术的触觉控制系统等医疗设备就是两个这样的例子。这些系统中的数值误差可能是灾难性的。丰田怀疑这些错误导致了其最近代价高昂的意外加速问题，阿丽亚娜5号火箭爆炸是由于其惯性参考系统溢出。该项目探索了测试和分析数值软件的实用技术，这将推动工程中最先进的强大数值软件，以帮助避免昂贵的，危险的错误。该项目特别关注数值误差的两个最基本的来源：未捕获的异常和数值稳定性和准确性。提出的核心框架以符号执行为中心，领域洞察力将用于开发原则和启发式，使其具有实用性。该项目将完成几项初步研究任务，以验证和证明拟议的一般方法的前景。它将探索数值精度和稳定性的新问题建模策略，研究现实的数值约束，以建立约束解决策略和算法的见解，并改进有前途的阿里阿德涅符号分析基础设施。

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.