|||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 ]|
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 |
full text on HAL |
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
|||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 ]|
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
Journal of Automated Reasoning, pages 1--29, 2014.
[ bib |
full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic