Verified Software

Nat Karmios is a PhD Student and Research Engineer in Imperial’s Verified Software Group under Professor Philippa Gardner, working on debugging and usability for symbolic execution tools.

After earning their MEng in Computing at Imperial—completing their thesis project with the group—Nat has brought their years of industry engineering experience to improve Gillian’s accessibility through the development of a visual debugger for Gillian. Their work continues: refining the Gillian debugging experience, exploring debugging applicability to other tools, and investigating links between tool usability and PL theory.

Group Publications

1. Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees

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

   Proceedings of the 32^nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, held as part of the International Joint Conferences on Theory and Practice of Software (TACAS 2026), pp. 195–214

2. Symbolic Debugging with Gillian

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

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