Scaling symbolic execution using ranged analysis

J. H. Siddiqui and S. Khurshid
ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA 2012)

Abstract

This paper introduces a novel approach to scale symbolic execution—a program analysis technique for systematic ex- ploration of bounded execution paths—for test input gener- ation. While the foundations of symbolic execution were de- veloped over three decades ago, recent years have seen a real resurgence of the technique, specifically for systematic bug finding. However, scaling symbolic execution remains a pri- mary technical challenge due to the inherent complexity of the path-based exploration that lies at core of the technique. Our key insight is that the state of the analysis can be rep- resented highly compactly: a test input is all that is needed to effectively encode the state of a symbolic execution run. We present ranged symbolic execution, which embodies this insight and uses two test inputs to define a range, i.e., the beginning and end, for a symbolic execution run. As an ap- plication of our approach, we show how it enables scalabil- ity by distributing the path exploration—both in a sequential setting with a single worker node and in a parallel setting with multiple workers. As an enabling technology, we lever- age the open-source, state-of-the-art symbolic execution tool KLEE. Experimental results using 71 programs chosen from the widely deployed GNU Coreutils set of Unix utilities show that our approach provides a significant speedup over KLEE. For example, using 10 worker cores, we achieve an average speed-up of 6.6X for the 71 programs.
(OOPSLA 2012), Tucson, AZ, October 2012. (Acceptance rate: 25%, 57/228) (Nominated for Best Student Paper Award)

BibTex

@inproceedings { oopsla2012,
author = { }, }