Skip to Main content Skip to Navigation
Conference papers

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
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:49:54 PM
Last modification on : Wednesday, November 20, 2019 - 2:40:16 AM
Document(s) archivé(s) le : Sunday, April 4, 2010 - 9:00:02 PM


  • HAL Id : inria-00072115, version 1



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⟩



Record views


Files downloads