TY - JOUR
T1 - Corrigendum
T2 - C-language floating-point proofs layered with VST and Flocq
AU - Appel, Andrew W.
AU - Bertot, Yves
N1 - Publisher Copyright:
© 2020,Journal of Formalized Reasoning. All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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. Mu˜noz, Aaron Dutle and François Bobot. A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm. In Formal Methods – 22nd International Symposium, 2018. Mariano M. Moscato, Laura Titolo, Marco A. Feliu, and Cesar A. Mu˜noz. A Provably Correct Floating-Point Implemntation of a Point-in-Polygon Algorithm.
AB - 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. Mu˜noz, Aaron Dutle and François Bobot. A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm. In Formal Methods – 22nd International Symposium, 2018. Mariano M. Moscato, Laura Titolo, Marco A. Feliu, and Cesar A. Mu˜noz. A Provably Correct Floating-Point Implemntation of a Point-in-Polygon Algorithm.
UR - http://www.scopus.com/inward/record.url?scp=85126950848&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85126950848&partnerID=8YFLogxK
U2 - 10.6092/ISSN.1972-5787/12643
DO - 10.6092/ISSN.1972-5787/12643
M3 - Comment/debate
AN - SCOPUS:85126950848
SN - 1972-5787
VL - 13
JO - Journal of Formalized Reasoning
JF - Journal of Formalized Reasoning
IS - 1
ER -