I was tidying up my emails at work and by coincidence I found the original paper that I was referring to, it's very pertinent to this discussion and interesting too, The pitfalls of verifying floating-point computations David Monniaux (LIENS, Verimag - Imag) http://arxiv.org/abs/cs/0701192