@inproceedings{MTDM2017,
author="Moscato, Mariano
and Titolo, Laura
and Dutle, Aaron
and Mu{\~{n}}oz, C{\'e}sar A.",
editor="Tonetta, Stefano
and Schoitsch, Erwin
and Bitsch, Friedemann",
title="Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis",
bookTitle="Computer Safety, Reliability, and Security: 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings",
series="Lecture Notes in Computer Science",
year="2017",
volume="10488",
publisher="Springer International Publishing",
address="Cham",
pages="213--229",
abstract="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.",
isbn="978-3-319-66266-4",
doi="10.1007/978-3-319-66266-4_14",
url="https://doi.org/10.1007/978-3-319-66266-4_14"
}