Improving assurance of high-consequence systems using formal methods and automated reasoning 

Error from imperfect computer representations of numbers when visualizing a sphere at 1km and 20,000km distance from an observer.
Error from imperfect computer representations of numbers when visualizing a sphere at 1km and 20,000km distance from an observer.

Computers typically represent numbers one of two ways: fixed-point (via integers) and floating-point numbers. Floating point provides improved efficiency and productivity, but errors can accumulate if not managed carefully. Error from floating point is called roundoff error and has caused loss of life in past high-consequence systems. Sandia researchers investigated techniques for automatically computing the worst-case roundoff error for computer programs. Research in collaboration with the University of Oregon resulted in improved techniques for understanding this error across all possible inputs. Sandia researchers led a collaboration with Oak Ridge National Laboratory, Pacific Northwest National Laboratory, NASA, and the French Commission for Atomic Energy to develop improvements to existing specification languages for roundoff error. These improvements will permit better analysis of floating-point roundoff errors.

COOL FACT > This project will improve the safety and reliability of high-consequence embedded control systems while maintaining capability and programmer productivity.

Sandia experts linked to work

  • Samuel D. Pollard

July 14, 2025