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

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

Publication Date

2023

Keywords

debugging, verification, symbolic execution

Identifiers

Source Materials