Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY

Nathalie Revol 1 K. Makino M. Berz
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : The goal of this paper is to prove that the implementation of Taylor models in COSY, based on floating-point arithmetic, computes results satisfyin- g the «containment property», i.e. guaranteed results. First, Taylor models are defined and their implementation in the COSY software by Makino and Berz is detailed. Afterwards IEEE-754 floating-point arithmetic is introduced. Then the core of this paper is given: the algorithms implemented in COSY for multiplying a Taylor model by a scalar, for adding or multiplying two Taylor models are given and are proven to return Taylor models satisfying the containment property.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00071850
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:57:22 PM
Last modification on : Monday, April 29, 2019 - 11:02:18 AM

Identifiers

  • HAL Id : inria-00071850, version 1

Collections

Citation

Nathalie Revol, K. Makino, M. Berz. Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY. [Research Report] RR-4737, LIP RR-2003-11, INRIA, LIP. 2003. ⟨inria-00071850⟩

Share

Metrics

Record views

178

Files downloads

315