Bio

I'm currently a Research Consultant at Adelard LLP where I evaluate, specify, and verify the implementations of safety-critical systems (e.g., autonomous systems, nuclear power plants, avionics, medical devices, etc.). I specialize in software and system analysis, verification, and model-checking, as well as carry-out safety and security assessments. In addition, I contribute to the production of standards and guidelines for safety and security related applications and their development.

I received my Computer Science PhD at University College London in January 2018, and I was advised by Nir Piterman. My work focused on the temporal verification, termination, and non-termination of infinite-state software 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

Thesis

"The Past, Present, and Future(s): Verifying Temporal Software Properties", Heidy Khlaaf. PhD Dissertation. Department of Computer Science, University College London, 2018. PDF

Research

Disruptive Innovations and Disruptive Assurance: Assuring Machine Learning and Autonomy R. Bloomfield and H. Khlaaf with P. Ryan Conmy, G. Fletcher. IEEE Computer, 52(9): 82-89 (2019).

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. 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. 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. 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. PDF

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

Tech

"Applicable and Achievable Formal Verification"
SRECon 2019 Keynote Speaker, Dublin, Ireland, 2019. (~800 attendees)

"Standards We Love"
Papers We Love @ Strangeloop, Invited Speaker, St. Louis, Missouri, 2018. (~500 attendees)

"Lessons from F#: From Academic Prototypes to Safety-Critical Systems"
F# eXchange, Invited Speaker, London, UK, 2018.

"Determining Software Safety in Critical Systems"
Github Constellation, Invited Speaker, London, UK, 2018. (~350 attendees)

Academic

"T2: Temporal Property Verification". Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, Netherlands, 2016.

"On Automation of CTL* Verification for Infinite-State Systems". Computer Aided Verification, San Francisco, USA, 2015. Best Paper Award.

"Fairness for Infinite-State Systems". Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom, 2015.

"Faster Temporal Reasoning for Infinite-State Programs". Formal Methods in Computer-Aided Design, Lausanne, Switzerland, 2014.

For a comprehensive list, please refer to my CV.

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/V9 grade range outdoors. I climb both indoors and outdoors and my most recent trips have been to: Rocklands (South Africa), the Peak District UK, Dolomites Italy, Sintra Portugal, Magic Wood Switzerland, Albarracin Spain, Shawangunk Mountains, Brione Switzerland, Sardegna Italy, Fontainebleau France, Yosemite National Park, Grand Canyon National Park.