PRECiSA with Instrumented Code Generation(LAR-19739-1)

PRECiSA (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.