Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees
Authors
- Nat Karmios
- Sacha-Élie Ayoun
- Philippa Gardner
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.
Venue
Proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, held as part of the International Joint Conferences on Theory and Practice of Software (TACAS 2026), pp. 195–214
Publication Date
Apr 2026