Symbolic Debugging with Gillian


  • Nat Karmios
  • Sacha-Élie Ayoun
  • Philippa Gardner


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.


Proceedings of the 1st ACM International Workshop on Future Debugging Techniques, pp. 1–2

Publication Date



debugging, verification, symbolic execution


Source Materials