Engineering Papers⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20205009218

Automatic Generation of Guard-Stable Floating-Point Code

Laura Titolo·Mariano Moscato·Marco A Feliu·Cesar A Munoz
View original source ↗Export metadata ↓

Abstract

The source did not provide an abstract. Follow the original record for more information.

Explore related subjects

Floating-Point ArithmeticRound-off errorsFormal VerificationTheorem ProvingStatic AnalysisFormal methodssoftware verification

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Laura Titolo, Mariano Moscato, Marco A Feliu, Cesar A Munoz. Automatic Generation of Guard-Stable Floating-Point Code. https://ntrs.nasa.gov/citations/20205009218

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRSDate not supplied

Automatic Generation of Guard-Stable Floating-Point Code

In floating-point programs, test instability occurs when the control flow of a conditional statement diverges from its ideal execution under real arithmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle test instability often require expertise on finite precision computations and rounding errors. This paper presents a fully automatic tool chain that generates and formally verifies a test-stable floating-point C program from its functional specification in real arithmetic. The generated program is instrumented to soundly detect when unstable tests may occur and, in these cases, to issue a warning. The proposed approach combines the PRECiSA floating-point static analyzer, the Frama-C software verification suite, and the PVS theorem prover.

Floating-Point Arithmetic↗