Skip to Main content Skip to Navigation

On formal methods for certifying floating-point C programs

Ali Ayad 1, 2, 3, *
* Corresponding author
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.
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download
Contributor : Claude Marché <>
Submitted on : Wednesday, May 13, 2009 - 3:43:31 PM
Last modification on : Wednesday, September 16, 2020 - 5:06:56 PM
Long-term archiving on: : Monday, October 15, 2012 - 10:16:45 AM


Files produced by the author(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⟩



Record views


Files downloads