Photo of Sacha Ayoun
  Webpage   s.ayoun17@imperial.ac.uk   GitHub Profile

Sacha was a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He completed his PhD in 2025.

As an undergraduate, Sacha worked at the French Alternative and Atomic Energy Commission (CEA) as a researcher-engineer intern in 2017. His goal was to improve the Frame-C abstract interpreter to better handle file descriptors. In 2018 he completed his Supelec Engineer Diploma at CentraleSupelec as well as his MSc in Advanced Computing at Imperial.

Group Publications

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

    Proceedings of the 32nd 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. Compositional Symbolic Execution for the Next 700 Memory Models

    Proc. ACM Program. Lang., vol. 9(OOPSLA2)

  3. Matching Plans for Frame Inference in Compositional Reasoning

    38th European Conference on Object-Oriented Programming (ECOOP 2024), pp. 26:1–26:20

  4. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

    38th European Conference on Object-Oriented Programming (ECOOP 2024), pp. 25:1–25:28

  5. Symbolic Debugging with Gillian

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

  6. Gillian, Part II: Real-World Verification for JavaScript and C

    Proceedings of the 33rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II, pp. 827–850

  7. Gillian, Part I: A Multi-language Platform for Symbolic Execution

    Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15–20, 2020, London, UK