[4] Sylvie Boldo and Jean-Michel Muller. Des ordinateurs capables de calculer plus juste. La Recherche, 492:46--52, October 2014. [ bib | full text on HAL ]
[3] Claude Marché. Verification of the functional behavior of a floating-point program: an industrial case study. Science of Computer Programming, 96(3):279--296, March 2014. [ bib | DOI | full text on HAL | .pdf ]
We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving

[2] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ]
[1] Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, pages 1--29, 2014. [ bib | DOI | full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic