PRECiSA

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 System (PVS).

PRECiSA is publicly available under NASA's Open Source Agreement from GitHub. Try PRECiSA online.

Publications

• Laura Titolo, Mariano Moscato, Marco Feliú, and César Muñoz, Automatic Generation of Guard-Stable Floating-Point Code, Proceedings 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. Lecture Notes in Computer Science, Vol. 11408, pp. 169-183, 2018. BibTeX 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.

The tag identifies links that are outside the NASA domain