On formal methods for certifying floating-point C programs

Ali Ayad 1, 2, 3, *
* Auteur correspondant
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Liste complète des métadonnées

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

Contributeur : Claude Marché <>
Soumis le : mercredi 13 mai 2009 - 15:43:31
Dernière modification le : jeudi 7 février 2019 - 15:02:29
Document(s) archivé(s) le : lundi 15 octobre 2012 - 10:16:45


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00383793, version 1



Ali Ayad. On formal methods for certifying floating-point C programs. [Research Report] RR-6927, INRIA. 2009, pp.34. 〈inria-00383793〉



Consultations de la notice


Téléchargements de fichiers