On formal methods for certifying floating-point C programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2009

On formal methods for certifying floating-point C programs

Résumé

This paper presents an implementation of an extension of the ACSL specication language in the Frama-C tool in order to prove the correctness of floating-point C programs. A first model checks that there is no over flow, i.e., proof obligations are generated by the Why tool to prove that the result of a fl oating-point operation is not greater than the maximal fl oat allowed in the given type, this model is called the Strict model. A second model, called the Full model, extends the Strict model. The Full model allows over flows and deals with special values: signed infinities, NaNs (Not-a-Number) and signed zeros as in the IEEE-754 Standard. The verification conditions generated by Why are (partially) proved by automatic theorem provers: Alt-Ergo, Simplify, Yices, Z3, CVC3 and Gappa or discharged in the interactive proof assistant Coq [20] using two existing Coq formalization of fl oating-point arithmetic. When the Why proof obligations are written in the syntax of the Gappa library, we can use the gappa and interval tactics to achieve the proof. Several examples of fl oating-point C programs are presented in the paper to prove the efficiency of this implementation.
Fichier principal
Vignette du fichier
RR-6927.pdf (279.19 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00383793 , version 1 (13-05-2009)

Identifiants

  • HAL Id : inria-00383793 , version 1

Citer

Ali Ayad. On formal methods for certifying floating-point C programs. [Research Report] RR-6927, INRIA. 2009, pp.34. ⟨inria-00383793⟩
479 Consultations
297 Téléchargements

Partager

Gmail Facebook X LinkedIn More