Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2014

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

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (207.5 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00967124 , version 1 (28-03-2014)

Identifiants

Citer

Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study. Science of Computer Programming, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩. ⟨hal-00967124⟩
276 Consultations
476 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More