The pitfalls of verifying floating-point computations
<|reference_start|>The pitfalls of verifying floating-point computations: 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.<|reference_end|>
@article{monniaux2007the,
    title={The pitfalls of verifying floating-point computations},
    author={David Monniaux (LIENS, Verimag - Imag)},
    journal={ACM Transactions on Programming Languages and Systems 30, 3 (2008)
  12},
    year={2007},
    doi={10.1145/1353445.1353446},
    archivePrefix={arXiv},
    eprint={cs/0701192},
    primaryClass={cs.PL cs.NA}
}