By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point

By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2017-November/001444.html http://lists.forge.open-do.org/pipermail/spark2014-discuss/2... Lots of links to recent stuff, you should look it all... If you have the time :-D.