Eliminating unstable tests in floating-point programs

DOI10.1007/978-3-030-13838-7_10zbMATH Open1524.68104arXiv1808.04289MaRDI QIDQ6085981

Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César Muñoz

Publication date: 9 November 2023

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Abstract: Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.

Full work available at URL: https://arxiv.org/abs/1808.04289

zbMATH Keywords

round-off error formal verification program transformation floating-point numbers test instability

Mathematics Subject Classification ID

Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)