Bio

I'm currently a Consultant at Adelard LLP where I evaluate, specify, and verify the implementations of safety-critical systems (e.g., nuclear, aviation, medical, etc.). My role includes consultancy, research, and training in safety and security related systems. Additionally I contribute to the production of standards and guidelines for safety and security related applications and their development. At Adelard, I specialize in software and system analysis, verification, and model-checking, as well as carry-out safety and security assessments.

My Computer Science PhD dissertation was submitted at University College London in September 2017, where I was advised by Nir Piterman and Alexandra Silva. My work focused on the temporal verification, termination, and non-termination of infinite-state systems. As a PhD student, I collaborated with Microsoft Research Cambridge as part of the PPT group to create and extend the T2 tool to support temporal property verification.

I received my Bachelor of Science from Florida State University where I obtained degrees in both Computer Science and Philosophy, with a minor in Mathematics.

Download CV

Research

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems H. Khlaaf with B. Cook and N. Piterman. Journal of ACM, 64, 2, Article 15 (May 2017), 39 pages.

"T2: Temporal Property Verification" M. Brockschmidt and H. Khlaaf with B. Cook, S. Ishtiaq, and N. Piterman Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, Netherlands, 2016. SLIDES | PDF

"On Automation of CTL* Verification for Infinite-State Systems" H. Khlaaf with B. Cook and N. Piterman. Computer Aided Verification, San Francisco, USA, 2015. Best Paper Award at CAV 2015, Invited Submission to JACM. SLIDES | PDF

"Fairness for Infinite-State Systems" H. Khlaaf with B. Cook and N. Piterman. Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom, 2015. SLIDES | PDF

"Faster Temporal Reasoning for Infinite-State Programs" H. Khlaaf with B. Cook and N. Piterman. Formal Methods in Computer-Aided Design, Lausanne, Switzerland, 2014. SLIDES | PDF

"Abstract: Fairness for Infinite-State Systems" H. Khlaaf with B. Cook and N. Piterman. 14th International Workshop on Termination, Vienna, Austria, 2014.

Climbing

When not analyzing safety-critical systems, you will most likely find me climbing. I mostly enjoy bouldering and I am currently climbing around the V8+ grade range outdoors. I climb both indoors and outdoors and my most recent trips have been to: Sintra Portugal, MagicWood Switzerland, Albarracin Spain, Shawangunk Mountains, Brione Switzerland, Sardegna Italy, Fontainebleau France, Yosemite National Park, Grand Canyon National Park, and the Peak District UK.