Verifying critical numerical software involves the generation of test data for floating-point
intensive programs. As the symbolic execution of floating-point computations presents
significant difficulties, existing approaches usually resort to random or search-based test
data generation. However, without symbolic reasoning, it is almost impossible to generate
test inputs that execute many paths with floating-point computations. Moreover, constraint
solvers over the reals or the rationals do not handle the rounding errors. In this paper, we …

… • FPSE and first experimental results … Our approach to solve path conditions : Interval
propagation over floating-point variables … Symbolic path-oriented test input generation on
FP-computations is feasible! …