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.
Design and Integration Tools
Linux, OS X
Contact Us About This Technology
Langley Research Center