Key Technology Research On Symbolic Execution Of Floating-point Programs

Symbolic execution of floating-point programs is challenging due to the limited support of backend solvers.This paper presents hotspot symbolic execution(HSE)to scale the symbolic execution of floating-point programs.The essential idea of HSE is to(1)explore the paths of some functions(called hotspot functions)in priority,and(2)divide the paths of a hotspot function into different equivalence classes,and explore as fewer path as possible inside the function while ensuring the coverage of all the classes.We have implemented HSE on KLEE and carried out extensive experiments on all 5528 functions in GNU Scientifc Library(GSL).The experimental results demonstrate the effectiveness and efficiency of HSE.Compared with the baseline,HSE detects >12 times of exceptions in 30 minutes.