Many contemporary verification tools make simplifying and simplistic assumptions about data types such as bit-vectors and floating point numbers. Such assumptions may result in imprecise abstractions that thwart successful verification or fail to account for corner cases responsible for intricate bugs. The goal of the proposed project is to apply as well as improve bit-level accurate decision procedures (SAT and SMT) to enable interpolation-based model checking as well as the detection and analysis of comlicated bugs for software that uses bit-vectors and floating point arithmetic.