Emily Yu
Leiden Institute of Advanced Computer Science (LIACS), Universität Leiden, Niederlande.
Kontakt:
z.yu@liacs.leidenuniv.nl
Ich bin Assistant Professor mit Tenure in Informatik an der Universität Leiden in den Niederlanden.
Meine Forschung entwickelt breit gefasst formale Methoden und automatisierte Schlussfolgerungsverfahren für den Bau vertrauenswürdiger Systeme. Ein zentrales Thema meiner Arbeit ist Zertifizierung: unabhängig prüfbare Nachweise, die Verifikationsprozesse für sicherheitskritische Systeme zuverlässiger und transparenter machen.
Meine Arbeit zur Zertifizierung hat die Entwicklung von Infrastruktur für Hardware Model Checking und Solver-Zuverlässigkeit beeinflusst. Diese Forschungslinie erhielt Distinguished Paper Awards auf der CAV 2025 und CAV 2026, der renommiertesten Konferenz im Bereich formale Verifikation. Außerdem wurde meine Forschung durch das Veni Talent Program des Dutch Research Council (NWO) in den Niederlanden und das hochkompetitive ESPRIT Fellowship des Austrian Science Fund (FWF) in Österreich ausgezeichnet.
Vor meiner Zeit in Leiden war ich Postdoktorandin (2023-2025) in der Gruppe von Prof. Thomas Henzinger am Institute of Science and Technology Austria. Ich habe im Doktoratsprogramm “Logical Methods in Computer Science” (LogiCS), gefördert durch den FWF, und am LIT AI Lab promoviert. Betreut wurde ich von Prof. Armin Biere an der Johannes Kepler Universität Linz in Österreich. Meine Dissertation beschäftigte sich mit Zertifizierung im Hardware Model Checking. Davor habe ich mein Bachelorstudium am Department of Computing des Imperial College London in Großbritannien abgeschlossen, wo ich von Prof. Alessio Lomuscio betreut wurde.
Interesse an einer Promotion bei mir? Schreiben Sie mir gerne eine E-Mail mit Ihrem Lebenslauf, Ihrem Transcript und einer kurzen Erklärung, wie Ihre Forschungsinteressen zum Veritas Lab passen. Zusätzlich kann es Möglichkeiten geben, sich für ein CSC-Stipendium zu bewerben.
Forschungsrichtungen
Meine Forschung entwickelt praktische Methoden, um festzustellen, ob komplexe Systeme sicher und korrekt sind, und um überprüfbare Belege für ihre Ergebnisse zu liefern. Meine Arbeit konzentriert sich auf vier miteinander verbundene Richtungen:
Laufzeitüberwachung
Manche Systeme können vor ihrem Einsatz nicht vollständig analysiert werden, insbesondere wenn ihre Dynamik unbekannt ist. Wir entwickeln Monitore, die ihr Verhalten beobachten, Sicherheitsverletzungen vorhersagen und rechtzeitiges Eingreifen ermöglichen.
Automatisiertes Schließen und Model Checking
Wir untersuchen, wie automatisierte Reasoning-Technologien wie SAT, SMT und Model Checking die skalierbare Verifikation sicherheitskritischer Systeme ermöglichen können.
KI-Verifikation
KI-Modelle sind leistungsfähig, doch ihre Entscheidungen sind oft schwer zu verstehen und abzusichern. Wir entwickeln Methoden zur Prüfung ihrer Sicherheit, Robustheit und Fairness sowie leichter verifizierbare Lernarchitekturen.
Zertifizierung
Verifikationswerkzeuge sind selbst komplex und können Fehler enthalten. Wir entwickeln formale Beweise und unabhängige Prüfer, damit Verifikationsergebnisse kompakte, maschinenprüfbare Korrektheitsnachweise enthalten.
Ausgewahlte Publikationen
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! |