10.6092/issn.1972-5787/12643
application/pdf
1972-5787
12643
1
en
Yves Bertot
http://creativecommons.org/licenses/by/3.0
Journal of Formalized Reasoning
Corrigendum: C floating-point proofs layered with VST and Flocq 
Text.Serial.Journal
https://jfr.unibo.it/
13
Errata
2021-03-31
2021-03-30
2020-12-21
2021-04-01
JFR
Yves Bertot
2020
10.6092/issn.1972-5787/12643
INRIA Sophia-Antipolis
1972-5787
1
en
Corrigendum: C floating-point proofs layered with VST and Flocq 
https://jfr.unibo.it/article/download/12643/12459
13
Corrigendum: C-language floating-point proofs
layered with VST and Flocq
Andrew W. Appel
Princeton University
and
Yves Bertot
INRIA and Université Côte d’Azur




   It has come to the authors’attention that citation STF+19 is to the wrong paper;
that paper is not connected to Frama-C and does not verify C code. More relevant
related work would include the following, both of which use PVS (to relate real-
number algorithms to floating-point algorithms) and Frama-C (to relate floating-
point algorithms to C code):
Laura Titolo, Mariano M. Moscato, Cesar A. Muñoz, Aaron Dutle and François
Bobot. A Formally Verified Floating-Point Implementation of the Compact Posi-
tion Reporting Algorithm. In Formal Methods – 22nd International Symposium,
2018.
Mariano M. Moscato, Laura Titolo, Marco A. Feliu, and Cesar A. Muñoz. A
Provably Correct Floating-Point Implemntation of a Point-in-Polygon Algorithm.
In Formal Methods – 23rd International Symposium, 2019.
