  Deductive verification has been successful in verifying interesting
properties of real-world programs. One notable gap is the limited support for
floating-point reasoning. This is unfortunate, as floating-point arithmetic is
particularly unintuitive to reason about due to rounding as well as the
presence of the special values infinity and `Not a Number' (NaN). In this
paper, we present the first floating-point support in a deductive verification
tool for the Java programming language. Our support in the KeY verifier handles
arithmetic via floating-point decision procedures inside SMT solvers and
transcendental functions via axiomatization. We evaluate this integration on
new benchmarks, and show that this approach is powerful enough to prove the
absence of floating-point special values -- often a prerequisite for further
reasoning about numerical computations -- as well as certain functional
properties for realistic benchmarks.
