The pitfalls of verifying floating-point computations

Fuente: arXiv
Guardado en:
Detalles Bibliográficos
Autor principal: Monniaux, David
Formato: Preprint
Publicado: 2007
Materias:
Acceso en línea:
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
_version_ 1866918162798215168
author Monniaux, David
author_facet Monniaux, David
contents Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.
format Preprint
id arxiv_https___arxiv_org_abs_cs_0701192
institution arXiv
publishDate 2007
record_format arxiv
spellingShingle The pitfalls of verifying floating-point computations
Monniaux, David
Programming Languages
Numerical Analysis
D.2.4; D.3.1; F.3.1; G.1.0; G.4
Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.
title The pitfalls of verifying floating-point computations
topic Programming Languages
Numerical Analysis
D.2.4; D.3.1; F.3.1; G.1.0; G.4
url https://arxiv.org/abs/cs/0701192