Gillian debugging: swinging through the (Compositional symbolic execution) trees
File(s)
Published version
Author(s)
Karmios, Nat
Ayoun, Sacha-Élie
Gardner, Philippa
Type
Chapter
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.
Date Issued
2026-04-15
Citation
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2026, 2026, pp.195-214
ISBN
9783032227485
Publisher
Springer Nature Switzerland
Start Page
195
End Page
214
Journal / Book Title
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2026
Lecture Notes in Computer Science
Copyright Statement
© The Author(s) 2026. This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License (http://creativecommons.org/licenses/by-nc-nd/4.0/), which permits any noncommercial use, sharing, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if you modified the licensed material. You do not have permission under this license to share adapted material derived from this chapter or parts of it.
Publication Status
Published
Date Publish Online
2026-04-15