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.