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

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.