Emily Yu
Leiden Institute of Advanced Computer Science (LIACS), Leiden University, Netherlands.
To reach me:
z.yu@liacs.leidenuniv.nl
I am a tenured assistant professor in Computer Science at Leiden University in the Netherlands.
My research broadly develops formal methods and automated reasoning techniques for building trustworthy systems. A central theme of my work is certification - designing independently checkable evidence that makes verification process more reliable and transparent for safety-critical systems. My work on certification has influenced the development of hardware model checking infrastructure and solver reliability. This line of work received Distinguished Paper Awards at CAV 2025 and CAV 2026, the most prestigious conference in formal verification. Additionally, my research has been recognized with the Dutch Research Council (NWO) Veni Talent Program in the Netherlands, and the highly competitive ESPRIT fellowship from the Austrian Science Fund (FWF) in Austria.
Before joining Leiden, I was a postdoctoral researcher (2023-2025) in Prof. Thomas Henzinger’s group at the Institute of Science and Technology Austria. I received my PhD in 2023 in the doctoral program ‘Logical Methods in Computer Science’ (LogiCS) funded by FWF, and the LIT AI Lab under the supervision of Prof. Armin Biere, at the Johannes Kepler University Linz in Austria. My thesis was on hardware model checking certification. Before that, I completed my undergraduate studies in the Department of Computing at Imperial College London, UK, where I was advised by Prof. Alessio Lomuscio.
Interested in doing a PhD with me? Please feel free to get in touch by email with your CV, transcript, and a brief note explaining how your research interests align with the Veritas Lab. Additionally, there may also be opportunities to apply for a CSC scholarship.
Research Directions
My research develops practical ways to understand whether complex systems are safe and correct, and to provide evidence that their results can be trusted. My work centers on four connected directions:
Runtime Monitoring
Some systems cannot be fully analyzed before deployment, especially when their dynamics are unknown. We develop monitors that observe their behavior, predict safety violations, and support timely intervention.
Automated Reasoning and Model Checking
We investigate how automated reasoning technologies such as SAT, SMT, and model checking can enable the verification of safety-critical systems at scale.
AI Verification
AI models are powerful, but their decisions can be difficult to understand and guarantee. We develop methods for checking their safety, robustness, and fairness, and design learning architectures that are easier to verify.
Certification
Verification tools are themselves complex and may contain bugs. We develop formal proofs and independent checkers so that verification results come with compact, machine-checkable evidence of correctness.
Featured Publications
news
| Jul 2026 | Our CAV 2026 paper, “Liveness Proofs for Hardware Model Checking”, received the Distinguished Paper Award! Looking forward to presenting this work in Lisbon. |
|---|---|
| Jul 2026 | I have been awarded an NWO Veni grant to support my research on certification for infinite-state systems for the next few years. |
| Jul 2026 | I will give a lecture at the upcoming IPA Fall Days, a dutch PhD school that I help organize, in November! The lecture will be on formal methods and AI. |
| Jun 2026 | Two papers accepted at FLOC 2026. Looking forward to seeing you in Lisbon! |
| Apr 2026 | I will be giving a series of 6 lectures at the SETSS spring school 2026! |