EAGER: Toward Numerically Robust Software

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

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.