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.