Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study

Claude Marché 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : 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.
Document type :
Journal articles
Science of Computer Programming, Elsevier, 2014, 93 (3), pp.279-296. 〈10.1016/j.scico.2014.04.003〉
Liste complète des métadonnées

Cited literature [44 references]  Display  Hide  Download

https://hal.inria.fr/hal-00967124
Contributor : Claude Marché <>
Submitted on : Friday, March 28, 2014 - 9:08:45 AM
Last modification on : Thursday, February 9, 2017 - 3:56:56 PM
Document(s) archivé(s) le : Saturday, June 28, 2014 - 10:56:34 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study. Science of Computer Programming, Elsevier, 2014, 93 (3), pp.279-296. 〈10.1016/j.scico.2014.04.003〉. 〈hal-00967124〉

Share

Metrics

Record views

242

Document downloads

212