SHF: Small: Testing and Analysis for Reliable Numerical Software

University Of California-Davis, Davis CA

Investigators

Abstract

Society increasingly depends on numerical software, which uses finite precision arithmetic to approximate the reals and necessarily introduces approximation and error. Cyber-physical systems are ubiquitous and rely on numerical software. 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 costly acceleration problem; the Ariane 5 rocket exploded due to an overflow in its inertial reference system; and scientists have had to retract papers from prestigious journals (e.g., Nature). Techniques and tools for improving numerical software reliability are critically needed. This project explores practical techniques to test and analyze numerical software. It focuses on the two most fundamental sources of numerical errors: uncaught exceptions, and numerical stability and accuracy. The proposed techniques are centered around symbolic execution and guided testing, and domain insights are used to develop principles and heuristics to make the techniques practical. This project considers three main dimensions: (1) problem formulation and analysis strategies, (2) constraint solving, and (3) implementation techniques. It aims at advancing the state-of-the-art in engineering robust numerical software to help avoid costly, dangerous errors.