Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic

David Monniaux, Alice Pain

Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which…