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.
Type de document :
Article dans une revue
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

Littérature citée [44 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00967124
Contributeur : Claude Marché <>
Soumis le : vendredi 28 mars 2014 - 09:08:45
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : samedi 28 juin 2014 - 10:56:34

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

244