3D Visualization of Symbolic Execution Traces

Symbolic execution is a powerful software testing technique for finding bugs in complex software. Unfortunately, following the symbolic execution and understanding its results is challenging. However, since symbolic execution is commonly not complete (i.e. due to path explosion) it is important to understand the limitations of the performed analysis. Otherwise, insufficiently tested code parts may not be identified and bugs remain unnoticed. Prior work attempts to address this problem via 2D visualizations which communicate properties of the performed analysis to the verification engineer. Since symbolic execution requires a visualization of several properties, such 2D visualizations often lack important information or end up being dense and difficult to understand. In order to overcome this limitation, we propose a novel 3D visualization of symbolic execution which allows visualizing additional properties via the third dimension. For this purpose, we have implemented a 3D visualization for the symbolic execution of RISC-V machine code and evaluate this implementation by comparing it to an existing 2D visualization. Our results demonstrate that the third dimension allows us to include additional information which is not captured by the existing 2D visualization. In order to stimulate further research on 3D visualization of symbolic execution, we have released our implementation as open source software.