Towards Quantification and Visualization of the Effects of Concretization During Concolic Testing

Concolic testing is a software testing technique, which improves the scalability of symbolic execution by allowing efficient concretization of symbolic expressions. Concretization converts a symbolic expression to a concrete value, e.g., when the constraints of a symbolic expression become too complex for the utilized solver to handle. Unfortunately, concretization negatively impacts completeness of the performed analysis. For example, if a branch in the tested program depends on a previously symbolic value, which is now concrete, this branch will not be tracked by the symbolic execution engine. As such, the tested code is not explored in its entirety and errors may remain undetected. In order to allow a verification engineer to identify code parts which have not been tested sufficiently, due to concretization, we propose a novel metric, which quantifies performed concretizations. Furthermore, we contribute a visualization of this metric, which eases identifying code parts, which depend, directly or indirectly, on symbolic values affected by concretization. To the best of our knowledge, this is the first work proposing a concretization metric for concolic testing, to stimulate further research on this topic we have released our implementation as open-source software.