Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Nat Karmios, Sacha-Élie Ayoun, Philippa Gardner

TL;DR

This work tackles the challenge of debugging compositional symbolic execution (CSE) outputs by introducing an interactive debugger integrated with Visual Studio Code for the Gillian platform. The approach combines a tree-of-trees execution representation, a source-level lifting mechanism, and a hybrid UI that extends the Debug Adapter Protocol with a custom interactive tree, enabling on-the-fly guidance of the analysis. Key contributions include a generalized, tool-agnostic debugging design, implementation insights such as structured logging and a continuation-based interpreter, and an empirical evaluation showing educational value and user-perceived usefulness. The work paves the way for broader adoption of SEDAP-style debugging across CSE tools and languages, with potential impact on teaching, tool development, and real-world verification tasks. The findings suggest that intuitive, interactive visualization of CSE, coupled with source-level mappings, can significantly aid understanding and debugging of heap-manipulating programs across languages like C, JavaScript, and Rust.

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.

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

TL;DR

This work tackles the challenge of debugging compositional symbolic execution (CSE) outputs by introducing an interactive debugger integrated with Visual Studio Code for the Gillian platform. The approach combines a tree-of-trees execution representation, a source-level lifting mechanism, and a hybrid UI that extends the Debug Adapter Protocol with a custom interactive tree, enabling on-the-fly guidance of the analysis. Key contributions include a generalized, tool-agnostic debugging design, implementation insights such as structured logging and a continuation-based interpreter, and an empirical evaluation showing educational value and user-perceived usefulness. The work paves the way for broader adoption of SEDAP-style debugging across CSE tools and languages, with potential impact on teaching, tool development, and real-world verification tasks. The findings suggest that intuitive, interactive visualization of CSE, coupled with source-level mappings, can significantly aid understanding and debugging of heap-manipulating programs across languages like C, JavaScript, and Rust.

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.
Paper Structure (29 sections, 4 equations, 7 figures, 4 tables)

This paper contains 29 sections, 4 equations, 7 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. The Gillian Debugging Experience
  5. Principles of CSE Debugging
  6. Low-level Tree-of-trees Structure
  7. Lifting to the Source Level
  8. User Interface
  9. Implementation Insights
  10. Structured logs.
  11. Rebuilding source-level commands.
  12. Advanced nesting.
  13. Everything is interactive.
  14. A generalised UI toolkit.
  15. Performance impact.
  16. ...and 14 more sections

Figures (7)

  • Figure 1: Slightly simplified SLL predicate and a specified WISL recursive list-length function (left), and the corresponding compiled GIL code, simplified (right). The prefix # denotes a logical variable.
  • Figure 2: Gillian's debugging and language server interface when verifying llen().
  • Figure 3: Full symbolic execution tree of llen()
  • Figure 4: Expanded failing node (left) and symbolic state at the failing match (right).
  • Figure 5: Overview: architecture of the Gillian debugger.
  • ...and 2 more figures