Verified Software

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

Xiaojia studied for his BA and MMath degree at the University of Cambridge and then moved to Imperial College London in 2020 to join the MSc in Advanced Computing. His Master’s thesis was on a verified model of WebAssembly in Coq called WasmCert-Coq.

Group Publications

1. Designing and Maintaining an Efficient WebAssembly Mechanisation

   • Xiaojia Rao

   Ph.D. Thesis, Imperial College London

2. Progressful Interpreters for Efficient WebAssembly Mechanisation

   • Xiaojia Rao
   • Stefan Radziuk
   • Conrad Watt
   • Philippa Gardner

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

3. Bringing the WebAssembly Standard up to Speed with SpecTec

   • Dongjun Youn
   • Wonho Shin
   • Jaehyun Lee
   • Sukyoung Ryu
   • Joachim Breitner
   • Philippa Gardner
   • Sam Lindley
   • Matija Pretnar
   • Xiaojia Rao
   • Conrad Watt
   • Andreas Rossberg

   Proceedings of the ACM on Programming Languages, Volume 8, Issue PLDI (PLDI 2024)

4. Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

   • Xiaojia Rao
   • Aïna Linn Georges
   • Maxime Legoupil
   • Conrad Watt
   • Jean Pichon-Pharabod
   • Philippa Gardner
   • Lars Birkedal

   44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), pp. 151:1–151:25

5. Two Mechanisations of WebAssembly 1.0

   • Conrad Watt
   • Xiaojia Rao
   • Jean Pichon-Pharabod
   • Martin Bodin
   • Philippa Gardner

   Proceedings of the 24^th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, pp. 61–79