Bio

Heidy Khlaaf is a Senior Research Consultant specializing in the evaluation, specification, and verification of software implementations in safety-critical systems, ranging from embedded devices to large nuclear power plants. She has led numerous safety and security audits (e.g., IEC 61508) that contribute to the assurance of safety-critical software, and has provided consultations and reviews of assurance cases across numerous industries. She specializes in software and system analysis, verification, and model-checking.

She additionally contributes to the production of standards and guidelines for safety and security related applications and their development. Most recently, she has contributed to AI governance approaches for the UK government through developing policy and regulatory frameworks that enable the safety assurance of disruptive technologies such as artificial intelligence and machine learning.

She received her Computer Science PhD at University College London in January 2018, where she was advised by Nir Piterman. Her work focused on the temporal verification, termination, and non-termination of infinite-state software systems. She has won a best paper award at CAV 2015, and a subsequent invitation to JACM, for her work on the first automated algorithm to verify CTL* verification for infinite-state systems. As a PhD student, she collaborated with Microsoft Research Cambridge to create and extend the T2 tool to support temporal property verification.

She received a Bachelor of Science from Florida State University for degrees in both Computer Science and Philosophy, with a minor in Mathematics, and graduated with honors and highest distinction.

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

Publications

"97 Things Every SRE Should Know", edited by Emil Stolarsky and Jaime Woo. O'Reilly Media Inc., November 2020.

Toward Trustworthy AI Development: Mechanisms for Supporting Verifiable Claims, April 2020. 59 co-authors from 29 organisations, including tech companies and academic groups such as: Open AI, Leverhulme Centre for the Future of Intelligence, University of Oxford, Partnership on AI, Adelard, Mila, Google Brain, and many others.

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

"Auditing safety-critical AI systems"
BSI-VdTÜV AI Forum On Auditing AI-Systems: From Basics to Applications (German Federal Office for Information Security ), Invited Speaker, Berlin, Germany, 2020. (~150 attendees)

"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: Portland UK, 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.