Front Page

Publications and Talks

PhD Research

Teaching and Students

Contact

Welcome to my page!

I enjoy developing logical models of software and hardware systems, and
formally proving their properties using interactive theorem provers such as
Isabelle/HOL, HOL4 and HOL Light.



Technical Skills:
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.



Academic Biography:
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.