Appel, A. W., & Bertot, Y. (2021). C floating-point proofs layered with VST and Flocq. Journal of Formalized Reasoning, 13(1), 1-16. https://doi.org/10.6092/issn.1972-5787/11442 (Original work published December 21, 2020)