Corrigendum: C-language floating-point proofs layered with VST and Flocq

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.