PRECiSA and ReFlow

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).

ReFlow is a fully automatic floating-point code extractor. Given a PVS real-valued program and the target floating-point precision (single or double), ReFlow generates the corresponding floating-point C implementation. The generated C code is annotated with ACSL (ANSI/ISO C Specification Language ) contracts that relate the floating-point implementation with the real-valued program specification. ReFlow relies on the static analyzer PRECiSA to compute sound round-off error estimations and the corresponding PVS proof certificate that guarantee their correctness.

PRECiSA and ReFlow are publicly available under NASA's Open Source Agreement from GitHub.

Publications

• Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, Mauricio Ayala-Rincón, A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023), pp. 237-246, TU Wien Academic Press, 2023. BibTeX Reference.
• 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