Program Round-Off Certifier via Static Analysis (PRECiSA) with Kodiak Integration(LAR-19227-1)

design and integration tools
Program Round-Off Certifier via Static Analysis (PRECiSA) with Kodiak Integration
PRECiSA, which in the current invention disclosure stands for Program Round-off Certifier via Static Analysis, is a fully automatic static analyzer for floating-point valued functions. It computes an over-approximation of the round-off error of a given floating-point expression, along with a formal certificate that ensures the correctness of the estimated error. The current invention extends PRECiSA in three ways:* it enables the use of external tools such as the global optimization tool Kodiak to compute numerical bounds in an efficient way,* it adds input language support for loops and recursion, and * it implements a more efficient analysis of nested conditionals.
Software Details

Design and Integration Tools
Reference Number
Release Type
Open Source
Operating System
Linux, OS X
Contact Us About This Technology

Langley Research Center
Stay up to date, follow NASA's Technology Transfer Program on:
facebook twitter linkedin youtube
Facebook Logo Twitter Logo Linkedin Logo Youtube Logo