SHF: Small: Testing and Analysis for Reliable Numerical Software

SHF：小型：可靠数值软件的测试和分析

• 批准号: 1618158
• 负责人: Zhendong Su
• 金额: $ 50万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-07-01 至 2019-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618158&HistoricalAwards=false
• 关键词: SHF; Small; Testing; Analysis; Reliable

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.

社会越来越依赖于数值软件，它使用有限精度的算法来近似实数，并不可避免地引入近似值和误差。网络物理系统无处不在，依赖于数字软件。防抱死制动和医疗设备，如触觉控制系统的远程手术是两个这样的例子。这些系统中的数值误差可能是灾难性的。 丰田怀疑这些错误导致了其昂贵的加速问题;阿丽亚娜5号火箭由于惯性参考系统溢出而爆炸;科学家不得不撤回来自著名期刊的论文（例如，Nature）。提高数值软件可靠性的技术和工具是迫切需要的。本项目探讨测试和分析数值软件的实用技术。 它集中在两个最基本的来源ofnumerical错误：未捕获的例外，和数值稳定性和准确性。所提出的技术是围绕symbolicexecution和引导测试，和域的见解是用来开发的原则和技巧，使技术实用。 该项目考虑三个主要方面：（1）问题的制定和分析策略，（2）约束解决，（3）实施技术。它的目的是推进工程鲁棒数值软件的最新技术，以帮助避免代价高昂的危险错误。