Symbolic crosschecking of floating-point and SIMD code
Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly · 2011
We present an effective technique for crosschecking an IEEE 754 floating-point program and its SIMD-vectorized version, implemented in KLEE-FP, an extension to the KLEE symbolic execution tool that supports symbolic reasoning on the equivalence between floating-point values.