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.
- Laura Titolo, Mariano Moscato, Marco Feliú, and César
Muñoz, Automatic Generation of Guard-Stable Floating-Point
of the 16th International Conference on Integrated Formal Methods
(iFM 2020), Lecture
Notes in Computer Science, Vol. 12546, pp. 141–159, 2020. BibTeX Reference.
- Laura Titolo, César Muñoz, Marco Feliú,
and Mariano Moscato, Eliminating Unstable Tests in Floating-Point Programs,
Proceedings of the 28th International Symposium on Logic-based
Program Synthesis and Transformation (LOPSTR 2018),
Frankfurt am Main, Germany, 2018.
Notes in Computer Science, Vol. 11408, pp. 169-183, 2018.
Reference. PVS 6.0 development
available here (Requires NASA PVS Library).
- Laura Titolo, Marco Feliu, Mariano Moscato, and César
Muñoz, An Abstract
Interpretation Framework for the Round-Off Error Analysis of
Floating-Point Programs, Proceedings of the 19th International Conference on
Verification, Model Checking, and Abstract Interpretation (VMCAI
2018), Lecture Notes in Computer Science,
Vol. 10747, pp. 516-537, 2018. BibTeX Reference.
- 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