I am a postdoctoral researcher at Azure Research (the former Confidential Computing group at Microsoft Research) interested in formal reasoning about relational security properties like noninterference (also called hyperproperties). I develop specification languages, verification and synthesis algorithms, as well as modeling and testing techniques. In particular, I work on principled methods to detect, model, and prevent information leakage through microarchtectural side channels.

I obtained my PhD from Saarland University (while working at CISPA) in 2022, where I was advised by Bernd Finkbeiner. My thesis was awarded with Saarland University’s Dr.-Eduard-Martin prize for the best computer science dissertation of the year. A 10-page summary of my thesis (with a focus on logics) can be found here.

News!

• October’23: I was awarded the Dr.-Eduard-Martin prize for best Computer Science Ph.D. thesis at Saarland University this year. For a 3-minute summary of my dissertation (in German) click here.
• October’23: I joined the PC of CAV 2024.
• July’23: Our paper Smart Contract Synthesis Modulo Hyperproperties won a Distinguished Paper Award at CSF’23! Find the paper here.
• July’23: Our paper Reactive Synthesis of Smart Contract Control Flows was accepted at ATVA’23!
• June’23: Our paper Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions was accepted at USENIX Security’23! See you in Anaheim!

Publications

• Reactive Synthesis of Smart Contract Control Flows
  With Bernd Finkbeiner, Noemi Passing, and Florian Kohn
  21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023).
• Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions
  With Emanuele Vannacci, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko
  USENIX Security 2023.
• Automata-Based Software Model Checking of Hyperproperties
  With Bernd Finkbeiner, Hadar Frenkel and Janine Lohse
  NASA Formal Methods (NFM 2023).
• Smart Contract Synthesis Modulo Hyperproperties
  With Norine Coenen, Bernd Finkbeiner and Julia Tillman
  36th IEEE Computer Security Foundations Symposium (CSF 2023).
  Distinguished Paper Award
• Logical Methods for the Hierarchy of Hyperlogics
  Dissertation, Saarland University, 2022.
  10-page summaries: English, German
  Dr.-Eduard-Martin prize
• Deciding Hyperproperties Combined with Functional Specifications
  With Raven Beutner, David Carral, Bernd Finkbeiner and Markus Krötzsch
  37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022).
• Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
  With Jonni Virtema, Bernd Finkbeiner, Juha Kontinen, and Fan Yang
  41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021).
• Runtime Enforcement of Hyperproperties
  With Norine Coenen, Bernd Finkbeiner, Christopher Hahn and Yannick Schillo
  19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021).
• The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
  With Norine Coenen, Bernd Finkbeiner and Christopher Hahn
  17th International Conference on Principles of Knowledge Representation and Reasoning, Recently Published Research Track (KR 2020).
• Realizing Omega-regular Hyperproperties
  With Bernd Finkbeiner, Christopher Hahn and Leander Tentrup
  32nd International Conference on Computer-Aided Verification (CAV 2020).
• The Hierarchy of Hyperlogics
  With Norine Coenen, Bernd Finkbeiner and Christopher Hahn
  34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019).

Presentations

• Formal Reasoning for the Detection of Microarchitectural Side Channels
  Invited talk at Woman@CL at Cambridge University, October 2023
• Smart Contract Synthesis Modulo Hyperproperties
  Paper presentation at CSF’23
• Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions
  
  • Invited talk at Seoul National University, October 2023
  • Invited talk at Stanford University, August 2023
  • Invited talk at CISPA Helmholtz Center for Information Security, May 2023
• Deciding Hyperproperties Combined with Functional Specifications
  Paper presentation at LICS’22
• Logics for the Specification of Hyperproperties
  Speaker at the 4th CISPA-LORIA workshop, April 2022
• The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
  Recently published research track at KR’22, YouTube recording
• Logics for Hyperproperties
  
  • Invited talk at IST Austria, July 2020
  • Invited talk at Tel Aviv University, September 2019
  • Invited talk at Yale University, July 2019
  • Invited talk at UC Berkeley, July 2019
• The Hierarchy of Hyperlogics
  Paper presentation at LICS’19

Teaching

Supervised Students

• Janine Lohse, Bachelor’s thesis: Model Checking for (Hyper) Temporal Stream Logic (2022)
• Yannick Schillo, Research project: Specifying Android Apps with TSL (2020 - 2022)
• Frederik Scheerer, Bachelor’s thesis: Monitoring Smart Contracts with RTLola (2021)
• Julia Tillman, Bachelor’s thesis: Temporal Stream Logic for Hyperproperties (2020)
• Matthias Cosler, Bachelor’s thesis: Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis (2019)

Assisted Lectures

During PhD

• Winter 2020/2021: Assistant for Basic Course Programmierung 1
  received Busy Beaver award for outstanding teaching performance
• Winter 2019/2020: Assistant for Core Course Verification
• Summer 2019: Advisor for Proseminar Softwarezuverlässigkeit (Software Reliability)
• Winter 2018/2019: Assistant for Seminar Hyperproperties

As Student

• Summer 2018: Coach for Mathematics Precourse at Saarland University
• Summer 2017: Lecturer and Coach for Mathematics Precourse at Saarland University
  BeStE award for student initiatives and extraordinary commitment
• Summer 2017: Student TA for Theoretical Computer Science at the School of Informatics, University of Edinburgh
• Winter 2016/2017: Student TA for Informatics I – Functional Programming at the School of Informatics, University of Edinburgh
• Summer 2016: Coach for Mathematics Precourse, Saarland University
• Summer 2016: Student TA for Concurrent Programming, Saarland University
• Winter 2015/2016: Organizer of Didactic Seminar for Re-exam Student TAs
• Winter 2015/2016: Supervision Student TA for Programming 1, Saarland University
• Summer 2015: Coach for Mathematics Precourse at Saarland University, Saarland University
• Winter 2014/2015: Organizer of Didactic Seminar for Re-exam Student TAs, Saarland University
• Winter 2014/2015: Student TA for Programming 1, Saarland University
• Winter 2013/2014: Re-exam Student TA for Programmierung 1, Saarland University

Scientific Service

• Program Committee: CAV’24, CSF’23, ICTAC’23, CAV’22 Artifact Evaluation
• External Reviewer: LICS’22, TACAS’21, MFCS’21, CONCUR’21, ATVA’21, CAV’21, LICS’21, CONCUR’20, KR’20, ICALP’20, TACAS’20, CSL’20, ATVA’19

Short CV

• Since Sep’22: Postdoctoral Researcher at Microsoft Research / Azure Research
• 2018 - 2022: Dr. rer. nat. at Saarland University / CISPA
• 2016 - 2017: M.Sc. in Computer Science at University of Edinburgh
• 2013 - 2016: B.Sc. in Computer Science at Saarland University