Welcome to my page!
I enjoy developing logical models of software and hardware systems, and
formally proving their properties using interactive theorem proving.
I mainly deal with low-level software visible hardware components,
operating system verification and compiler correctness.
I prove theorems in Isabelle/HOL, HOL4 and HOL Light theorem provers.
Talk to me about formal methods, formal verification, low-level programs and
embedded systems! :-)
These days, I am a postdoctoral researcher with Magnus Myreen in Division of Formal Methods, Chalmers University, Gothenburg. We are working on the project "m2mc: High-Confidence Formal Verification of Real Cyber-Physical Systems: from Models to Machine Code". The research goal of this project is to develop a new theoretical foundation of formally verified cyber-physical domain-specific model compilation, from high-level real system models down to machine code, satisfying both functional and temporal constraints.
I have completed my PhD from UNSW Sydney, also working with Trustworthy Systems, Data61, CSIRO under the supervision of Gerwin Klein. My research topic was related to low-level program verification in the presence of cached address translation. More information on my PhD is available here.
Before PhD, I completed my undergraduate and masters in Electrical Engineering from CEME, NUST, and SEECS, NUST, Islamabad. I conducted my master's research with Osman Hasan, the thesis is available at Publications and Talks.