This paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-off errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-off Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.
CITATION STYLE
Moscato, M., Titolo, L., Dutle, A., & Muñoz, C. A. (2017). Automatic estimation of verified floating-point round-off errors via static analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10488 LNCS, pp. 213–229). Springer Verlag. https://doi.org/10.1007/978-3-319-66266-4_14
Mendeley helps you to discover research relevant for your work.