Dr. Heidy Khlaaf is an Engineering Director at Trail of Bits specializing in the evaluation, specification, and verification of complex or autonomous software implementations in safety-critical systems, ranging from UAVs to large nuclear power plants. Her expertise ranges from leading numerous system safety audits (e.g., IEC 61508, DO-178C) that contribute to the assurance of safety-critical software within regulatory frameworks and safety cases, to bolstering the dependability and robustness of complex software systems through techniques such as system hazard analyses and formal verification to identify and mitigate for system and software risks.
She is known for her work leading the safety evaluation of Codex through developing a framework that measures a code generation models’ performance based on the the complexity of natural language specifications and integrating said performance outcomes within a cross-functional hazard analysis and risk assessment framework.
Her unique expertise at the intersection of Systems Software Engineering and Machine Learning has allowed her to lead, contribute, and produce the development of various standards and auditing frameworks for safety related applications and their development. This includes policy and regulatory frameworks for US and UK Regulators that enable the assurance of AI and ML to be safely deployed within critical systems. She is currently an ISO SC 42 (Artificial Intelligence) Committee Member via the British Standards Institute.
She completed her Computer Science PhD at University College London in 2017, where she was advised by Nir Piterman. She was a recipient of the prestigious NSF GRFP award. 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.
She received a Bachelor of Science from Florida State University for dual degrees in both Computer Science and Philosophy, with a minor in Mathematics, and graduated with honors and highest distinction.
"The Past, Present, and Future(s): Verifying Temporal Software Properties",
Heidy Khlaaf. PhD Dissertation. Department of Computer Science, University College London, 2018.
"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.
"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.
"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.
"Faster Temporal Reasoning for Infinite-State Programs"
H. Khlaaf* with B. Cook and N. Piterman. Formal Methods in Computer-Aided Design, Lausanne, Switzerland, 2014.
"Abstract: Fairness for Infinite-State Systems"
H. Khlaaf* with B. Cook and N. Piterman. 14th International Workshop on Termination, Vienna, Austria, 2014.
"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)
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.