PRECiSA (Program Round-off Error Certifier
via Static Analysis) is a fully automatic analyzer for
the estimation of round-off errors of floating-point valued functional
expressions. This research tool computes an over-approximation of
the round-off error of a given floating-point expression and also
generates a formal certificate that ensures the correctness of the
computed estimation. This certificate relies on a formalization of
floating-point arithmetic developed in the Prototype Verification
PRECiSA is publicly available under NASA's Open Source Agreement from GitHub. Try PRECiSA online.
- Mariano Moscato, Laura Titolo, Aaron Dutle, and César
Muñoz, Automatic Estimation of
Verified Floating-Point Round-Off Errors via Static
Analysis, Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017), Lecture Notes in Computer Science,
Vol. 10488, pp. 213-229, 2017. BibTeX Reference.
identifies links that are outside
the NASA domain