Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version
Nat Karmios, Sacha-\'Elie Ayoun, Philippa Gardner

TL;DR
This paper introduces a visual debugging interface for compositional symbolic execution tools, integrated with Visual Studio Code, enhancing understanding and verification of complex code structures.
Contribution
It presents a tool-agnostic debugging interface with visualization and interactivity for symbolic execution, tested through a user study demonstrating its effectiveness.
Findings
Improves understanding of CSE principles.
Helps verify data structure algorithms.
Enhances debugging experience in symbolic analysis.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Data Visualization and Analytics · Logic, programming, and type systems
