NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
an abstract interpretation framework for the round-off error analysis of floating-point programsThis paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.
Document ID
20180006290
Document Type
Conference Paper
Authors
Titolo, Laura
(National Inst. of Aerospace Hampton, VA, United States)
Feliu, Marco A.
(National Inst. of Aerospace Hampton, VA, United States)
Moscato, Mariano
(National Inst. of Aerospace Hampton, VA, United States)
Munoz, Cesar A.
(NASA Langley Research Center Hampton, VA, United States)
Date Acquired
October 16, 2018
Publication Date
January 8, 2018
Subject Category
Numerical Analysis
Report/Patent Number
NF1676-L-28210
Meeting Information
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)(Los Angeles, CA)
Funding Number(s)
WBS: WBS 999182.02.85.07.01
Distribution Limits
Public
Copyright
Public Use Permitted.

Available Downloads

NameType 20180006290.pdf STI