Hotspot symbolic execution of floating-point programs

Abstract

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 Scientific 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.

BibTeX

@inproceedings{Quan:FSE16,
  author    = {Minghui Quan},
  title     = {Hotspot symbolic execution of floating-point programs},
  booktitle = {FSE},
  pages     = {1112--1114},
  publisher = {{ACM}},
  year      = {2016},
}

Hotspot symbolic execution of floating-point programs

Abstract

Related papers