I'm a first year Computer Science PhD student at University College London where I'm co-advised by Byron Cook (Microsoft Research & UCL) and Peter O'Hearn (Facebook & UCL) as part of the PPLV group. Generally, I'm interested in Formal Verification, Separation Logic, Temporal Logic, and Termination. I'm currently discovering how procedure summarization, precondition synthesis, and traditional bottom up approaches complement each other to improve the performance and applicability of novel verification tools.

I am also a Research Contractor at Microsoft Research Cambridge where I work on Temporal Property Verification as part of the PPT group.

Previously, I received my Bachelor of Science from Florida State University where I double majored in Computer Science and Philosophy with a minor in Mathematics.


E-mail: [h dot khlaaf at ucl dot ac dot uk]