Symbolic Debugging with Gillian =============================== Authors ------- * Nat Karmios * Sacha-Élie Ayoun * Philippa Gardner Abstract -------- Software debugging for concrete execution enjoys a mature suite of tools, but debugging symbolic execution is still in its infancy. It carries unique challenges, as a single state can lead to multiple branches representing different sets of conditions, and symbolic states must be 'matched' against logical conditions. Some of today’s otherwise mature symbolic-execution tools still rely on plain-text log files for debugging, which provide no good overview of the execution process and can quickly become overwhelming. We introduce a debugger for Gillian’s verification mode---complete with a custom interface---and ponder the potential for this interface and the protocol behind it to be used outside of Gillian. Venue ----- International Workshop on Future Debugging Techniques (DEBT) Year ---- 2023 DOI --- * doi:`10.1145/3605155.3605861 `_