A. W. Appel and Y. Bertot, “C floating-point proofs layered with VST and Flocq”, JFR, vol. 13, no. 1, pp. 1–16, Jan. 2020.