SHF: Small: Testing and Analysis for Reliable Numerical Software

社会越来越依赖数字软件，它使用有限精度的算法来逼近实数，并必然引入逼近和误差。网络物理系统无处不在，依赖于数值软件。反锁装置和医疗设备，如用于远程手术的触觉控制系统，就是两个这样的例子。这些系统中的数字误差可能是灾难性的。丰田怀疑这些错误导致了其代价高昂的加速问题；阿丽亚娜5号火箭因惯性参考系统溢出而爆炸；科学家不得不撤回著名期刊(如《自然》)上的论文。迫切需要提高数值软件可靠性的技术和工具。本项目探索用于测试和分析数值软件的实用技术。它着重于数值误差的两个最基本的来源：未捕获的异常，以及数值的稳定性和准确性。所提出的技术以符号执行和引导测试为中心，并使用领域洞察来开发原理和启发式方法，使技术变得实用。这个项目考虑了三个主要维度：(1)问题表达和分析策略，(2)约束解决，和(3)实现技术。它的目标是在设计强大的数字软件方面推进最先进的技术，以帮助避免代价高昂的危险错误。

Society increasingly depends on numerical software, which uses finiteprecision arithmetic to approximate the reals and necessarilyintroduces approximation and error. Cyber-physical systems areubiquitous and rely on numerical software. Anti-lock breaks andmedical devices such as haptic control systems for remote surgery aretwo such examples. Numerical errors in these systems can bedisastrous. Toyota suspects such errors contributed to its costlyacceleration problem; the Ariane 5 rocket exploded due to an overflowin its inertial reference system; and scientists have had to retractpapers from prestigious journals (e.g., Nature). Techniques and toolsfor improving numerical software reliability are critically needed.This project explores practical techniques to test and analyzenumerical software. It focuses on the two most fundamental sources ofnumerical errors: uncaught exceptions, and numerical stability andaccuracy. The proposed techniques are centered around symbolicexecution and guided testing, and domain insights are used to developprinciples and heuristics to make the techniques practical. Thisproject considers three main dimensions: (1) problem formulation andanalysis strategies, (2) constraint solving, and (3) implementationtechniques. It aims at advancing the state-of-the-art in engineeringrobust numerical software to help avoid costly, dangerous errors.