Boosting Concolic Testing via Interpolation

Joxan Jaffar, Vijayaraghavan Murali and Jorge Navas

Abstract

Concolic testing has been very successful in au- tomatically generating test inputs for programs. However one of its major limitations is path-explosion that limits the generation of high coverage inputs. Since its inception sev- eral ideas have been proposed to attack this problem from various angles: defining search heuristics that increase cov- erage, caching of function summaries, pruning of paths us- ing static/dynamic information etc. We propose a new and complementary method based on interpolation, that greatly mitigates path-explosion by subsuming paths that can be guaranteed to not hit a bug. We discuss new challenges in using interpolation that arise specifically in the context of concolic testing. We experimentally evaluate our method with different search heuristics using Crest, a state-of-the- art concolic tester.