Software verification is an active and critical area of research in the field of computer science. Specifically, the verification of floating-point computations in programs is a problem of significant importance, given the widespread usage of floating-point arithmetic in both hardware and software applications. Despite this, there are relatively few verification tools that provide support for floating-point types. To help address this issue, we present the addition of floating-point support to the Boogie verification tool, which has achieved substantial prominence within the software verification community. We based this extension off of the SMT-LIB FloatingPoint theory and designed it to provide a human-readable Boogie syntax while being easily translatable to SMT-LIB format. We also used this extension to enable the SMACK verification toolchain to model the math.h functions in the C standard library. Finally, we tested the extension by leveraging SMACK and running it against a comprehensive set of floating-point benchmarks obtained from the Software Verification Competition (SV-COMP) 2017. We found that Boogie had superior performance to most other verification tools with floating-point support.