@article{Mon08b,
title = { The pitfalls of verifying floating-point computations },
author = {Monniaux, David},
month = {may},
year = {2008},
journal = {TOPLAS},
number = {3},
pages = {12},
publisher = {ACM},
volume = {30},
team = {SYNC,PACSS},
fjournal = {ACM Transactions on programming languages and systems},
fpublisher = {Association for Computing Machinery},
issn = {0164-0925},
pdf = {http://hal.archives-ouvertes.fr/docs/00/28/14/29/PDF/floating-point-article.pdf},
abstract = {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.},
}
