In recent years, compositional symbolic execution (CSE) tools have been growing in prominence and are becoming more and more applicable to real-world codebases. Still to this day, however, debugging the output of these tools remains difficult, even for specialist users. To address this, we introduce a debugging interface for symbolic execution tools, integrated with Visual Studio Code and the Gillian multi-language CSE platform, with strong focus on visualisation, interactivity, and intuitive representation of symbolic execution trees. We take care in making this interface tool-agnostic, easing its transfer to other symbolic analysis tools in future. We empirically evaluate our work with a user study, the results of which show the debugger's usefulness in helping early researchers understand the principles of CSE and verify fundamental data structure algorithms in Gillian.
翻译:近年来,组合符号执行工具的重要性日益凸显,并越来越多地应用于实际代码库。然而,即使对于专业用户而言,调试这些工具的输出结果至今仍具挑战性。为此,我们提出了一种集成于Visual Studio Code和Gillian多语言组合符号执行平台的符号执行调试界面,该界面高度注重符号执行树的可视化、交互性及直观呈现。我们致力于使该界面具备工具无关性,以便未来能更便捷地移植至其他符号分析工具。我们通过用户研究对工作进行了实证评估,结果表明该调试器能有效帮助初级研究者理解组合符号执行原理,并在Gillian平台上验证基础数据结构算法。