NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
automatic estimation of verified floating-point round-off errors via static analysisThis paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-o errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-o Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.
Document ID
20170009111
Document Type
Conference Paper
Authors
Moscato, Mariano
(National Inst. of Aerospace Hampton, VA, United States)
Titolo, Laura
(National Inst. of Aerospace Hampton, VA, United States)
Dutle, Aaron
(NASA Langley Research Center Hampton, VA, United States)
Munoz, Cesar A.
(NASA Langley Research Center Hampton, VA, United States)
Date Acquired
September 27, 2017
Publication Date
September 12, 2017
Subject Category
Numerical Analysis
Report/Patent Number
NF1676L-26663
Meeting Information
International Conference on Computer Safety, Reliability, and Security 2017(Trento)
Funding Number(s)
WBS: WBS 154692.02.50.07.01
Distribution Limits
Public
Copyright
Public Use Permitted.

Available Downloads

NameType 20170009111.pdf STI