Verified Software

Sacha Ayoun is a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner. He is currently working on Gillian, a parametric symbolic execution tool for symbolic testing, verification and automatic compositional testing.

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. Exact Separation Logic (submitted)

   • Petar Maksimovic
   • Caroline Cronjäger
   • Julian Sutherland
   • Andreas Lööw
   • Sacha-Élie Ayoun
   • Philippa Gardner

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

   • Petar Maksimovic
   • Sacha-Élie Ayoun
   • José Fragoso Santos
   • Philippa Gardner

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

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

   • José Fragoso Santos
   • Petar Maksimovic
   • Sacha-Élie Ayoun
   • Philippa Gardner

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