Welcome to my page!
Operating system kernel verification
Compiler implementation and verification
Reasoning about low-level programs in the presence of hardware details
These days, I am a postdoctoral researcher with
Magnus Myreen in Division of Formal Methods,
Chalmers University, Gothenburg.
We are developing Pancake: a Pascal-like language that compiles to the lower stack of
the CakeML compiler.
Pancake would be an imperative language with a simpler memory model and a formally verified implementation to develop low-level programs for real-time cyber-physical and embedded systems.
Github repository of the Pancake development
The development of Pancake is part of a joint research project with Model-based Computing Systems (MCS) group, KTH University, to develop a new theoretical foundation for formally verified cyber-physical model compilation satisfying both functional and temporal constraints.
I carried out my PhD research in UNSW Sydney with Gerwin Klein as the advisor, and also working with Trustworthy Systems, Data61, CSIRO. My PhD research addresses low-level program verification in the presence of cached address translation. More information on my PhD is available here.
I completed bachelors and masters in Electrical Engineering from CE&ME NUST and SEECS NUST respectively, and conducted my master's research with Osman Hasan, the thesis is available at Publications and Talks.