NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login

Press Enter or click the Search button to begin your search.

Back to Results
PRECiSA: a static analysis tool for floating-point programsThis presentation introduces PRECiSA, a static analysis framework for analyzing floating-point programs. PRECiSA computes round-off error bounds for a class of floating-point programs, and produces a formal proof certificate of the correctness of these bounds. PRECiSA also has the capability of generating C code which is instrumented to detect unstable branching conditions from a real-number algorithm specification.
Document ID
20220008765
Acquisition Source
Langley Research Center
Document Type
Presentation
Authors
Laura Titolo (National Institute of Aerospace Hampton, Virginia, United States)
Mariano Moscato (National Institute for Aerospace Technology Madrid, Spain)
Marco A. Feliu (National Institute of Aerospace Hampton, Virginia, United States)
Cesar A. Munoz (Langley Research Center Hampton, Virginia, United States)
Paolo Masci (National Institute of Aerospace Hampton, Virginia, United States)
Aaron Dutle (Langley Research Center Hampton, Virginia, United States)
Date Acquired
June 2, 2022
Subject Category
Computer Programming And Software
Meeting Information
Meeting: System-Wide Safety TC-3 Workshop
Location: Virtual
Country: US
Start Date: July 12, 2022
End Date: July 13, 2022
Sponsors: National Aeronautics and Space Administration
Funding Number(s)
WBS: WBS 340428.02.20.07.01
Distribution Limits
Public
Copyright
Use by or on behalf of the US Gov. Permitted.
Technical Review
NASA Peer Committee
Keywords
Floating-point
Formal methods

Related Records

IDRelationTitle20220009909See AlsoVSCode-PRECiSA: a Toolkit for Floating-Point Round-Off Error Analysis
No Preview Available