@InProceedings{TMFM2020,
author="Titolo, Laura
and Moscato, Mariano
and Feliu, Marco A.
and Mu{\~{n}}oz, C{\'e}sar A.",
editor="Dongol, Brijesh
and Troubitsyna, Elena",
title="Automatic Generation of Guard-Stable Floating-Point Code",
booktitle="Integrated Formal Methods",
year="2020",
publisher="Springer International Publishing",
series = "Lecture Notes in Computer Science",      
volume = "12546",
address="Cham",
pages="141--159",
abstract="In floating-point programs, guard instability occurs when the control flow of a conditional statement diverges from its ideal execution under real arithmetic. This phenomenon is caused by the presence of round-off errors in floating-point computations. Writing programs that correctly handle guard instability often requires expertise on finite precision arithmetic. This paper presents a fully automatic toolchain that generates and formally verifies a guard-stable floating-point C program from its functional specification in real arithmetic. The generated program is instrumented to soundly detect when unstable guards may occur and, in these cases, to issue a warning. The proposed approach combines the PRECiSA floating-point static analyzer, the Frama-C software verification suite, and the PVS theorem prover.",
doi="10.1007/978-3-030-63461-2_8",
isbn="978-3-030-63461-2"
}