Paper Info
Title
Properties of the subtraction valid for any floating point system
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 Sterbenzu0027s 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.
Year
DOI
Venue
2002
10.1016/S1571-0661(04)80408-0
Electronic Notes in Theoretical Computer Science
Keywords
Field
DocType
floating point
Digital signal processing,Computer science,Floating point,Avionics,Arithmetic,Automated proof checking,Theoretical computer science,Implementation,Subtraction,Formal proof
Journal
Volume
Issue
ISSN
66
2
1571-0661
Citations 
PageRank 
References 
2
0.46
5
Authors
2
Name
Order
Citations
PageRank
Sylvie Boldo129226.85
Marc Daumas221625.32