Questions tagged [floating-point]

Use this tag for floating point numbers as defined for use in a computer floating-point register. Do not use this tag for the mathematical concept of a floating point number.

Filter by
Sorted by
Tagged with
12 votes
3 answers

PDEs and proof assistants

I would like to know if there are any ongoing or completed projects in the area of the verification of the numerical methods for PDEs or the exposition of (any aspects of) the traditional PDE theory ...
user9716869 - supports Ukraine's user avatar
18 votes
2 answers

How can I prove facts about floating point calculations?

In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
wizzwizz4's user avatar
  • 495
12 votes
1 answer

Tools to check correctness of decimal floating point arithmetic

I have implemented (in TeX, but it doesn't matter for this question) a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating ...
Bruno Le Floch's user avatar