English

Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version

Programming Languages 2026-02-10 v1

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.

Keywords

Cite

@article{arxiv.2602.07742,
  title  = {Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees, Extended Version},
  author = {Nat Karmios and Sacha-Élie Ayoun and Philippa Gardner},
  journal= {arXiv preprint arXiv:2602.07742},
  year   = {2026}
}

Comments

24 pages, 11 figures. To be published at TACAS 2026

R2 v1 2026-07-01T10:26:20.577Z