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.