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

Andrew W. Appel, Yves Bertot

Research output: Contribution to journalComment/debatepeer-review


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.

Original languageEnglish (US)
JournalJournal of Formalized Reasoning
Issue number1
StatePublished - 2020

All Science Journal Classification (ASJC) codes

  • Computer Science (miscellaneous)
  • General Mathematics


Dive into the research topics of 'Corrigendum: C-language floating-point proofs layered with VST and Flocq'. Together they form a unique fingerprint.

Cite this