I'm a PhD candidate at UNSW Sydney, working in the Trustworthy Systems Group led by Prof. Gernot Heiser. My research focuses on verifying multithreaded network subsystems built on the seL4 secure microkernel, using Isabelle/HOL, rely-guarantee reasoning, and separation logic. I'm supervised by Dr. Rob Sison, Dr. Thomas Sewell, and Dr. Miki Tanaka.
2026
Samuel Tyler, Alessandro Legnani, Junming Zhao, Zhewen Shen, Rihui Wu, Miki Tanaka, and Gernot Heiser
14th Workshop on Programming Languages and Operating Systems (PLOS 2026). To appear.
2026
2025
Junming Zhao, Miki Tanaka, Johannes Åman Pohjola, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish, and Gernot Heiser
arXiv:2501.08249 [cs.PL].
2026
Renaissance Philanthropy AI for Math Summer Fellowship
Mechanising angelic nondeterminism in Isabelle/HOL and researching parallelism for angelic processes.
Supervised by Dr. Pedro Ribeiro.
2023 — 2024
UNSW Trustworthy Systems Group
Implemented Pancake device drivers and benchmarked network performance.
2022 — 2024
Ported MMTk to GHC and introduced flexible garbage-collection plans for functional-language runtimes.
Supervised by Prof. Steve Blackburn and Ben Gamari.
2024 — Present
University of New South Wales
2018 — 2023
The Australian National University
First Class Honours · University Medal