Properties of the subtraction valid for any floating point system

Sylvie Boldo 1 Marc Daumas
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We start in this text with a very generic definition of floating point systems. We show that just a few very natural necessary conditions are sufficient to focus down to two classes of implemented floating point arithmetic. Later, we prove that, for all the existing implementations, high level properties such as Sterbenz's theorem are satisfied. We finish this text by focusing on the differences between an IEEE-754 compatible unit and Texas Instrument TMS/SMJ 320C3x digital signal processing circuit that is recommended for avionics and military applications. The results presented in this text have been validated by the Coq automatic proof checker to build confidence for later implementations in critical systems such as an aircraft flight control primary or secondary computer.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00072115
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:49:54 PM
Last modification on : Wednesday, April 17, 2019 - 4:08:01 PM
Long-term archiving on : Sunday, April 4, 2010 - 9:00:02 PM

Identifiers

  • HAL Id : inria-00072115, version 1

Collections

Citation

Sylvie Boldo, Marc Daumas. Properties of the subtraction valid for any floating point system. 7th International Workshop on Formal Methods for Industrial Critical Systems, 2002, Málaga, Spain. pp.137-149. ⟨inria-00072115⟩

Share

Metrics

Record views

175

Files downloads

510